let k be Element of NAT ; :: thesis: for X being non empty set st k + 1 c= card X holds
for A being finite Subset of X st card A = k - 1 holds
^^ (A,X,k) is STAR

let X be non empty set ; :: thesis: ( k + 1 c= card X implies for A being finite Subset of X st card A = k - 1 holds
^^ (A,X,k) is STAR )

assume A1: k + 1 c= card X ; :: thesis: for A being finite Subset of X st card A = k - 1 holds
^^ (A,X,k) is STAR

let A be finite Subset of X; :: thesis: ( card A = k - 1 implies ^^ (A,X,k) is STAR )
assume A2: card A = k - 1 ; :: thesis: ^^ (A,X,k) is STAR
^^ (A,X,k) = ^^ (A,X) by ;
hence ^^ (A,X,k) is STAR by A2; :: thesis: verum
{"ft_lang_label":"__label__en","ft_lang_prob":0.7962485,"math_prob":0.9996544,"size":580,"snap":"2022-40-2023-06","text_gpt3_token_len":221,"char_repetition_ratio":0.1892361,"word_repetition_ratio":0.40939596,"special_character_ratio":0.42413792,"punctuation_ratio":0.15853658,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":1.0000055,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2022-10-02T15:55:19Z\",\"WARC-Record-ID\":\"<urn:uuid:71141f2d-d692-486f-a5e5-f70a1954d893>\",\"Content-Length\":\"7971\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:57374fa2-3b26-47ca-acb7-ec7d9b3c5e3a>\",\"WARC-Concurrent-To\":\"<urn:uuid:109d931b-fd34-4a8c-8de6-d147542de0ca>\",\"WARC-IP-Address\":\"193.219.28.149\",\"WARC-Target-URI\":\"http://mizar.org/version/current/html/proofs/combgras/44\",\"WARC-Payload-Digest\":\"sha1:CGJW4DA5BNEZBH4JHKFTG3LN7KNYZQRJ\",\"WARC-Block-Digest\":\"sha1:RYIZ6TOF544UFJRSXEYQPRWA2CKAJ57M\",\"WARC-Identified-Payload-Type\":\"application/xml\",\"warc_filename\":\"/cc_download/warc_2022/CC-MAIN-2022-40/CC-MAIN-2022-40_segments_1664030337338.11_warc_CC-MAIN-20221002150039-20221002180039-00077.warc.gz\"}"}