:: SCMYCIEL  semantic presentation begin  
theorem :: SCMYCIEL:1 (Bool  "for" (Set (Var "x")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "holds" (Bool (Bool  "not" (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "X")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "X"))))) ; 
 
theorem :: SCMYCIEL:2 (Bool  "for" (Set (Var "x")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "holds" (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "X")) ($#k4_tarski :::"]"::: ) )  ($#r1_hidden :::"<>"::: )  (Set (Var "X")))) ; 
 
theorem :: SCMYCIEL:3 (Bool  "for" (Set (Var "x")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "holds" (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "X")) ($#k4_tarski :::"]"::: ) )  ($#r1_hidden :::"<>"::: )  (Set (Var "x")))) ; 
 
theorem :: SCMYCIEL:4 (Bool  "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x1"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "x2"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "y1")) "," (Set (Var "X")) ($#k4_tarski :::"]"::: ) ) ($#k2_tarski :::"}"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x2")) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "y2")) "," (Set (Var "X")) ($#k4_tarski :::"]"::: ) ) ($#k2_tarski :::"}"::: ) ))) "holds"  (Bool  "("  (Bool (Set (Var "x1"))  ($#r1_hidden :::"="::: )  (Set (Var "x2"))) & (Bool (Set (Var "y1"))  ($#r1_hidden :::"="::: )  (Set (Var "y2")))  ")" )) ; 
 
theorem :: SCMYCIEL:5 (Bool  "for" (Set (Var "X")) "," (Set (Var "v")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Num 3)  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X"))))) "holds"  (Bool  "ex" (Set (Var "v1")) "," (Set (Var "v2")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "v1"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "v2"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "v1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "v"))) & (Bool (Set (Var "v2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "v"))) & (Bool (Set (Var "v1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "v2")))  ")" ))) ; 
 
theorem :: SCMYCIEL:6 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k9_bspace :::"singletons"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; 
 registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )   (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_finset_1 :::"finite"::: )   bbbadV2_FINSET_1()   ($#v1_finseq_1 :::"FinSequence-like"::: )     ($#v2_finseq_1 :::"FinSubsequence-like"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: SCMYCIEL:7 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "P")) "being"    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set (Var "X"))  "st" (Bool (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "P")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "X"))))) "holds"  (Bool  "ex" (Set (Var "p")) "," (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "p"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "p"))) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y")))  ")" )))) ; 
 registration
cluster (Set   ($#k3_tarski :::"Vertices"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; 
theorem :: SCMYCIEL:8 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ($#k2_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) ; 
 
theorem :: SCMYCIEL:9 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "s")) "is" (Num 1)  ($#v3_card_1 :::"-element"::: )  )) "holds"  (Bool  "ex" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "s"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))  ")" )))) ; 
 
theorem :: SCMYCIEL:10 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )   "{"  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "X")) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "X")) ($#k4_tarski :::"]"::: ) ) ($#k2_tarski :::"}"::: ) ) where x "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X")) : (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  "}"  )  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X"))))) ; 
 definitionlet "G" be    ($#m1_hidden :::"set"::: )  ; func  :::"PairsOf"::: "G" ->   ($#m1_subset_1 :::"Subset":::) "of" "G" means :: SCMYCIEL:def 1 (Bool  "for" (Set (Var "e")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "("  (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  "G") & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "e")))  ($#r1_hidden :::"="::: )  (Num 2))  ")" )  ")" )); end; 





:: deftheorem    defines :::"PairsOf"::: SCMYCIEL:def 1 :  (Bool  "for" (Set (Var "G")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_scmyciel :::"PairsOf"::: )  (Set (Var "G")))) "iff" (Bool  "for" (Set (Var "e")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set (Var "b2"))) "iff" (Bool  "("  (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set (Var "G"))) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "e")))  ($#r1_hidden :::"="::: )  (Num 2))  ")" )  ")" ))  ")" ))); 
 
theorem :: SCMYCIEL:11 (Bool  "for" (Set (Var "X")) "," (Set (Var "e")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_scmyciel :::"PairsOf"::: )  (Set (Var "X"))))) "holds"  (Bool  "ex" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y"))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "X")))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "X")))) & (Bool (Set (Var "e"))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ))  ")" ))) ; 
 
theorem :: SCMYCIEL:12 (Bool  "for" (Set (Var "X")) "," (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y"))) & (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k1_scmyciel :::"PairsOf"::: )  (Set (Var "X"))))) ; 
 
theorem :: SCMYCIEL:13 (Bool  "for" (Set (Var "X")) "," (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k1_scmyciel :::"PairsOf"::: )  (Set (Var "X"))))) "holds"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y"))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "X")))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "X"))))  ")" )) ; 
 
theorem :: SCMYCIEL:14 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "G"))  ($#r1_tarski :::"c="::: )  (Set (Var "H")))) "holds"  (Bool (Set   ($#k1_scmyciel :::"PairsOf"::: )  (Set (Var "G")))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_scmyciel :::"PairsOf"::: )  (Set (Var "H"))))) ; 
 
theorem :: SCMYCIEL:15 (Bool  "for" (Set (Var "X")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )   "{"  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "X")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#k2_tarski :::"}"::: ) ) where x, y "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k3_tarski :::"union"::: )  (Set (Var "X"))) : (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k1_scmyciel :::"PairsOf"::: )  (Set (Var "X"))))  "}"  )  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k1_scmyciel :::"PairsOf"::: )  (Set (Var "X")) ")" ) ")" )))) ; 
 
theorem :: SCMYCIEL:16 (Bool  "for" (Set (Var "X")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )   "{"  (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) where x, y "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k3_tarski :::"union"::: )  (Set (Var "X"))) : (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k1_scmyciel :::"PairsOf"::: )  (Set (Var "X"))))  "}"  )  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k1_scmyciel :::"PairsOf"::: )  (Set (Var "X")) ")" ) ")" )))) ; 
 registrationlet "X" be   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k1_scmyciel :::"PairsOf"::: )  "X") ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; attr "X" is  :::"void":::  means :: SCMYCIEL:def 2 (Bool "X"  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )); end; 




:: deftheorem    defines :::"void"::: SCMYCIEL:def 2 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v1_scmyciel :::"void"::: )  ) "iff" (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))  ")" )); 
 registration
cluster   ($#v1_scmyciel :::"void"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registration
cluster   ($#v1_scmyciel :::"void"::: )    ->   ($#v1_finset_1 :::"finite"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "G" be   ($#v1_scmyciel :::"void"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k3_tarski :::"Vertices"::: )  "G") ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; 
theorem :: SCMYCIEL:17 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_scmyciel :::"void"::: )  )) "holds"  (Bool (Set   ($#k1_scmyciel :::"PairsOf"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: SCMYCIEL:18 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "("   "not" (Bool (Set   ($#k3_tarski :::"union"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) "or" (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) "or" (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))  ")" )) ; 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; attr "X" is  :::"pairfree":::  means :: SCMYCIEL:def 3 (Bool (Set   ($#k1_scmyciel :::"PairsOf"::: )  "X") "is"   ($#v1_xboole_0 :::"empty"::: )  ); end; 




:: deftheorem    defines :::"pairfree"::: SCMYCIEL:def 3 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v2_scmyciel :::"pairfree"::: )  ) "iff" (Bool (Set   ($#k1_scmyciel :::"PairsOf"::: )  (Set (Var "X"))) "is"   ($#v1_xboole_0 :::"empty"::: )  )  ")" )); 
 
theorem :: SCMYCIEL:19 (Bool  "for" (Set (Var "X")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set (Var "X")) "is"   ($#v2_scmyciel :::"pairfree"::: )  )) ; 
 registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v5_finset_1 :::"finite-membered"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "X" be   ($#v5_finset_1 :::"finite-membered"::: )     ($#m1_hidden :::"set"::: )  ; let "Y" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set "X"  ($#k3_xboole_0 :::"/\"::: )  "Y") ->   ($#v5_finset_1 :::"finite-membered"::: )   ; 

cluster (Set "X"  ($#k4_xboole_0 :::"\"::: )  "Y") ->   ($#v5_finset_1 :::"finite-membered"::: )   ; 
end; begin  definitionlet "n" be   ($#m1_hidden :::"Nat":::); let "X" be    ($#m1_hidden :::"set"::: )  ; attr "X" is "n" :::"-at_most_dimensional":::  means :: SCMYCIEL:def 4 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "X")) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "x")))  ($#r1_ordinal1 :::"c="::: )  (Set "n"  ($#k1_nat_1 :::"+"::: )  (Num 1)))); end; 





:: deftheorem    defines :::"-at_most_dimensional"::: SCMYCIEL:def 4 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X")) "is" (Set (Var "n"))  ($#v3_scmyciel :::"-at_most_dimensional"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "x")))  ($#r1_ordinal1 :::"c="::: )  (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1))))  ")" ))); 
 registrationlet "n" be   ($#m1_hidden :::"Nat":::); 
cluster "n"  ($#v3_scmyciel :::"-at_most_dimensional"::: )    ->   ($#v5_finset_1 :::"finite-membered"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "n" be   ($#m1_hidden :::"Nat":::); 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_classes1 :::"subset-closed"::: )   "n"  ($#v3_scmyciel :::"-at_most_dimensional"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: SCMYCIEL:20 (Bool  "for" (Set (Var "G")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_classes1 :::"subset-closed"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "G")))) ; 
 
theorem :: SCMYCIEL:21 (Bool  "for" (Set (Var "n")) "being"   ($#v7_ordinal1 :::"natural"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "X")) "being" (Set (Var "b1"))  ($#v3_scmyciel :::"-at_most_dimensional"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1)))))) ; 
 registrationlet "n" be   ($#m1_hidden :::"Nat":::); let "X", "Y" be (Set (Const "n"))  ($#v3_scmyciel :::"-at_most_dimensional"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster (Set "X"  ($#k2_xboole_0 :::"\/"::: )  "Y") -> "n"  ($#v3_scmyciel :::"-at_most_dimensional"::: )   ; 
end; registrationlet "n" be   ($#m1_hidden :::"Nat":::); let "X" be (Set (Const "n"))  ($#v3_scmyciel :::"-at_most_dimensional"::: )     ($#m1_hidden :::"set"::: )  ; let "Y" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set "X"  ($#k3_xboole_0 :::"/\"::: )  "Y") -> "n"  ($#v3_scmyciel :::"-at_most_dimensional"::: )   ; 

cluster (Set "X"  ($#k4_xboole_0 :::"\"::: )  "Y") -> "n"  ($#v3_scmyciel :::"-at_most_dimensional"::: )   ; 
end; registrationlet "n" be   ($#m1_hidden :::"Nat":::); let "X" be (Set (Const "n"))  ($#v3_scmyciel :::"-at_most_dimensional"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster   -> "n"  ($#v3_scmyciel :::"-at_most_dimensional"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  "X"); 
end; definitionlet "s" be    ($#m1_hidden :::"set"::: )  ; attr "s" is  :::"SimpleGraph-like":::  means :: SCMYCIEL:def 5 (Bool  "("  (Bool "s" "is" (Num 1)  ($#v3_scmyciel :::"-at_most_dimensional"::: )  ) & (Bool "s" "is"   ($#v1_classes1 :::"subset-closed"::: )  ) & (Bool (Bool  "not" "s" "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")" ); end; 




:: deftheorem    defines :::"SimpleGraph-like"::: SCMYCIEL:def 5 :  (Bool  "for" (Set (Var "s")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "s")) "is"   ($#v4_scmyciel :::"SimpleGraph-like"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "s")) "is" (Num 1)  ($#v3_scmyciel :::"-at_most_dimensional"::: )  ) & (Bool (Set (Var "s")) "is"   ($#v1_classes1 :::"subset-closed"::: )  ) & (Bool (Bool  "not" (Set (Var "s")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")" )  ")" )); 
 registration
cluster   ($#v4_scmyciel :::"SimpleGraph-like"::: )    ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_classes1 :::"subset-closed"::: )   (Num 1)  ($#v3_scmyciel :::"-at_most_dimensional"::: )    for    ($#m1_hidden :::"set"::: )  ; 

cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_classes1 :::"subset-closed"::: )   (Num 1)  ($#v3_scmyciel :::"-at_most_dimensional"::: )    ->   ($#v4_scmyciel :::"SimpleGraph-like"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: SCMYCIEL:22 (Bool (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) "is"   ($#v4_scmyciel :::"SimpleGraph-like"::: )  ) ; 
 registration
cluster (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) ->   ($#v4_scmyciel :::"SimpleGraph-like"::: )   ; 
end; registration
cluster   ($#v4_scmyciel :::"SimpleGraph-like"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; definitionmode SimpleGraph is   ($#v4_scmyciel :::"SimpleGraph-like"::: )     ($#m1_hidden :::"set"::: )  ; end; registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v5_finset_1 :::"finite-membered"::: )   bbbadV2_FINSUB_1() bbbadV1_SETFAM_1()   ($#v1_classes1 :::"subset-closed"::: )     ($#v1_scmyciel :::"void"::: )   (Num 1)  ($#v3_scmyciel :::"-at_most_dimensional"::: )     ($#v4_scmyciel :::"SimpleGraph-like"::: )    for    ($#m1_hidden :::"set"::: )  ; 

cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )     ($#v5_finset_1 :::"finite-membered"::: )   bbbadV2_FINSUB_1() bbbadV1_SETFAM_1()   ($#v1_classes1 :::"subset-closed"::: )   (Num 1)  ($#v3_scmyciel :::"-at_most_dimensional"::: )     ($#v4_scmyciel :::"SimpleGraph-like"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; notationlet "G" be    ($#m1_hidden :::"set"::: )  ; synonym  :::"Vertices"::: "G" for  :::"union"::: "G"; synonym  :::"Edges"::: "G" for  :::"PairsOf"::: "G"; end; notationlet "X" be    ($#m1_hidden :::"set"::: )  ; synonym  :::"edgeless"::: "X" for  :::"pairfree"::: ; end; 
theorem :: SCMYCIEL:23 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  "st" (Bool (Bool (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "G"))) "is"   ($#v1_finset_1 :::"finite"::: )  )) "holds"  (Bool (Set (Var "G")) "is"   ($#v1_finset_1 :::"finite"::: )  )) ; 
 
theorem :: SCMYCIEL:24 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "G")))) "iff" (Bool (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "G")))  ")" ))) ; 
 
theorem :: SCMYCIEL:25 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ($#k2_tarski :::"}"::: ) ) "is"   ($#m1_hidden :::"SimpleGraph":::))) ; 
 definitionlet "X" be   ($#v1_finset_1 :::"finite"::: )     ($#v5_finset_1 :::"finite-membered"::: )     ($#m1_hidden :::"set"::: )  ; func  :::"order"::: "X" ->   ($#m1_hidden :::"Nat":::) equals :: SCMYCIEL:def 6 (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k3_tarski :::"union"::: )  "X" ")" )); end; 





:: deftheorem    defines :::"order"::: SCMYCIEL:def 6 :  (Bool  "for" (Set (Var "X")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#v5_finset_1 :::"finite-membered"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k2_scmyciel :::"order"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "X")) ")" )))); 
 definitionlet "X" be   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )  ; func  :::"size"::: "X" ->   ($#m1_hidden :::"Nat":::) equals :: SCMYCIEL:def 7 (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k1_scmyciel :::"PairsOf"::: )  "X" ")" )); end; 





:: deftheorem    defines :::"size"::: SCMYCIEL:def 7 :  (Bool  "for" (Set (Var "X")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k3_scmyciel :::"size"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k1_scmyciel :::"PairsOf"::: )  (Set (Var "X")) ")" )))); 
 
theorem :: SCMYCIEL:26 (Bool  "for" (Set (Var "G")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"SimpleGraph":::) "holds"  (Bool (Set   ($#k2_scmyciel :::"order"::: )  (Set (Var "G")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "G"))))) ; 
 definitionlet "G" be   ($#m1_hidden :::"SimpleGraph":::); mode Vertex of "G" is    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k3_tarski :::"Vertices"::: )  "G"); mode Edge of "G" is    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_scmyciel :::"Edges"::: )  "G"); end; 
theorem :: SCMYCIEL:27 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::) "holds"  (Bool (Set (Var "G"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set  "("  ($#k9_bspace :::"singletons"::: )  (Set  "("  ($#k3_tarski :::"Vertices"::: )  (Set (Var "G")) ")" ) ")" ) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "("  ($#k1_scmyciel :::"Edges"::: )  (Set (Var "G")) ")" )))) ; 
 
theorem :: SCMYCIEL:28 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  "st" (Bool (Bool (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set (Var "G")) "is"   ($#v1_scmyciel :::"void"::: )  )) ; 
 
theorem :: SCMYCIEL:29 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "G"))) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool  "("   "for" (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "("   "not" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) )) "or"  "not" (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "G"))))  ")" )  ")" )) "holds"  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_scmyciel :::"Edges"::: )  (Set (Var "G")))))) ; 
 
theorem :: SCMYCIEL:30 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) "holds"  (Bool (Set (Var "G"))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ($#k2_tarski :::"}"::: ) )))) ; 
 
theorem :: SCMYCIEL:31 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   (Bool  "ex" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::) "st"  (Bool  "("  (Bool (Set (Var "G")) "is"   ($#v2_scmyciel :::"edgeless"::: )  ) & (Bool (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set (Var "X")))  ")" ))) ; 
 definitionlet "G" be   ($#m1_hidden :::"SimpleGraph":::); let "v" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Const "G"))); func  :::"Adjacent"::: "v" ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_tarski :::"Vertices"::: )  "G" ")" ) means :: SCMYCIEL:def 8 (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k3_tarski :::"Vertices"::: )  "G") "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool (Set  ($#k2_tarski :::"{"::: ) "v" "," (Set (Var "x")) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k1_scmyciel :::"Edges"::: )  "G"))  ")" )); end; 






:: deftheorem    defines :::"Adjacent"::: SCMYCIEL:def 8 :  (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "v")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "G")))  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_tarski :::"Vertices"::: )  (Set (Var "G")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_scmyciel :::"Adjacent"::: )  (Set (Var "v")))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "G"))) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b3"))) "iff" (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "v")) "," (Set (Var "x")) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k1_scmyciel :::"Edges"::: )  (Set (Var "G"))))  ")" ))  ")" )))); 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; mode  :::"SimpleGraph":::  "of" "X" ->   ($#m1_hidden :::"SimpleGraph":::) means :: SCMYCIEL:def 9 (Bool (Set   ($#k3_tarski :::"Vertices"::: )  it)  ($#r1_hidden :::"="::: )  "X"); end; 





:: deftheorem    defines :::"SimpleGraph"::: SCMYCIEL:def 9 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#m1_hidden :::"SimpleGraph":::) "holds"   (Bool  "("  (Bool (Set (Var "b2")) "is"    ($#m1_scmyciel :::"SimpleGraph"::: )   "of" (Set (Var "X"))) "iff" (Bool (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set (Var "X")))  ")" ))); 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; func  :::"CompleteSGraph"::: "X" ->    ($#m1_scmyciel :::"SimpleGraph"::: )   "of" "X" equals :: SCMYCIEL:def 10  "{"  (Set (Var "V")) where V "is"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" "X" : (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "V")))  ($#r1_xxreal_0 :::"<="::: )  (Num 2))  "}"  ; end; 





:: deftheorem    defines :::"CompleteSGraph"::: SCMYCIEL:def 10 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k5_scmyciel :::"CompleteSGraph"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "V")) where V "is"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "V")))  ($#r1_xxreal_0 :::"<="::: )  (Num 2))  "}"  )); 
 
theorem :: SCMYCIEL:32 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "G")))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "G"))))) "holds"  (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "G")))  ")" )) "holds"  (Bool (Set (Var "G"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_scmyciel :::"CompleteSGraph"::: )  (Set  "("  ($#k3_tarski :::"Vertices"::: )  (Set (Var "G")) ")" )))) ; 
 registrationlet "X" be   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k5_scmyciel :::"CompleteSGraph"::: )  "X") ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; 
theorem :: SCMYCIEL:33 (Bool  "for" (Set (Var "X")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k5_scmyciel :::"CompleteSGraph"::: )  (Set (Var "X"))))) ; 
 
theorem :: SCMYCIEL:34 (Bool  "for" (Set (Var "X")) "," (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k5_scmyciel :::"CompleteSGraph"::: )  (Set (Var "X"))))) ; 
 
theorem :: SCMYCIEL:35 (Bool (Set   ($#k5_scmyciel :::"CompleteSGraph"::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) ; 
 
theorem :: SCMYCIEL:36 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k5_scmyciel :::"CompleteSGraph"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ($#k2_tarski :::"}"::: ) ))) ; 
 
theorem :: SCMYCIEL:37 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k5_scmyciel :::"CompleteSGraph"::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k2_enumset1 :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) "," (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ) ($#k2_enumset1 :::"}"::: ) ))) ; 
 
theorem :: SCMYCIEL:38 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) "holds"  (Bool (Set   ($#k5_scmyciel :::"CompleteSGraph"::: )  (Set (Var "X")))  ($#r1_tarski :::"c="::: )  (Set   ($#k5_scmyciel :::"CompleteSGraph"::: )  (Set (Var "Y"))))) ; 
 
theorem :: SCMYCIEL:39 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "G"))))) "holds"  (Bool (Set   ($#k5_scmyciel :::"CompleteSGraph"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))  ($#r1_tarski :::"c="::: )  (Set (Var "G"))))) ; 
 registrationlet "G" be   ($#m1_hidden :::"SimpleGraph":::); 
cluster   ($#v5_finset_1 :::"finite-membered"::: )   (Num 1)  ($#v3_scmyciel :::"-at_most_dimensional"::: )     ($#v4_scmyciel :::"SimpleGraph-like"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  "G"); 
end; definitionlet "G" be   ($#m1_hidden :::"SimpleGraph":::); mode Subgraph of "G" is   ($#v4_scmyciel :::"SimpleGraph-like"::: )    ($#m1_subset_1 :::"Subset":::) "of" "G"; end; definitionlet "G" be   ($#m1_hidden :::"SimpleGraph":::); func  :::"Complement"::: "G" ->   ($#m1_hidden :::"SimpleGraph":::) equals :: SCMYCIEL:def 11 (Set (Set  "("  ($#k5_scmyciel :::"CompleteSGraph"::: )  (Set  "("  ($#k3_tarski :::"Vertices"::: )  "G" ")" ) ")" )  ($#k6_subset_1 :::"\"::: )  (Set  "("  ($#k1_scmyciel :::"Edges"::: )  "G" ")" )); involutiveness  
(Bool  "for" (Set (Var "b1")) "," (Set (Var "b2")) "being"   ($#m1_hidden :::"SimpleGraph":::)  "st" (Bool (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_scmyciel :::"CompleteSGraph"::: )  (Set  "("  ($#k3_tarski :::"Vertices"::: )  (Set (Var "b2")) ")" ) ")" )  ($#k6_subset_1 :::"\"::: )  (Set  "("  ($#k1_scmyciel :::"Edges"::: )  (Set (Var "b2")) ")" )))) "holds"  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_scmyciel :::"CompleteSGraph"::: )  (Set  "("  ($#k3_tarski :::"Vertices"::: )  (Set (Var "b1")) ")" ) ")" )  ($#k6_subset_1 :::"\"::: )  (Set  "("  ($#k1_scmyciel :::"Edges"::: )  (Set (Var "b1")) ")" ))))
 ; end; 





:: deftheorem    defines :::"Complement"::: SCMYCIEL:def 11 :  (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::) "holds"  (Bool (Set   ($#k6_scmyciel :::"Complement"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_scmyciel :::"CompleteSGraph"::: )  (Set  "("  ($#k3_tarski :::"Vertices"::: )  (Set (Var "G")) ")" ) ")" )  ($#k6_subset_1 :::"\"::: )  (Set  "("  ($#k1_scmyciel :::"Edges"::: )  (Set (Var "G")) ")" )))); 
 
theorem :: SCMYCIEL:40 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::) "holds"  (Bool (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"Vertices"::: )  (Set  "("  ($#k6_scmyciel :::"Complement"::: )  (Set (Var "G")) ")" )))) ; 
 
theorem :: SCMYCIEL:41 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y"))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "G")))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "G"))))) "holds"  (Bool  "("  (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k1_scmyciel :::"Edges"::: )  (Set (Var "G")))) "iff" (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"nin"::: )  (Set   ($#k1_scmyciel :::"Edges"::: )  (Set  "("  ($#k6_scmyciel :::"Complement"::: )  (Set (Var "G")) ")" )))  ")" ))) ; 
 begin  definitionlet "G" be   ($#m1_hidden :::"SimpleGraph":::); let "L" be    ($#m1_hidden :::"set"::: )  ; func "G" :::"SubgraphInducedBy"::: "L" ->   ($#m1_subset_1 :::"Subset":::) "of" "G" equals :: SCMYCIEL:def 12 (Set "G"  ($#k3_xboole_0 :::"/\"::: )  (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  "L" ")" )); end; 






:: deftheorem    defines :::"SubgraphInducedBy"::: SCMYCIEL:def 12 :  (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "L")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "G"))  ($#k7_scmyciel :::"SubgraphInducedBy"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "G"))  ($#k3_xboole_0 :::"/\"::: )  (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  (Set (Var "L")) ")" ))))); 
 registrationlet "G" be   ($#m1_hidden :::"SimpleGraph":::); let "L" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set "G"  ($#k7_scmyciel :::"SubgraphInducedBy"::: )  "L") ->   ($#v4_scmyciel :::"SimpleGraph-like"::: )   ; 
end; 
theorem :: SCMYCIEL:42 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::) "holds"  (Bool (Set (Var "G"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "G"))  ($#k7_scmyciel :::"SubgraphInducedBy"::: )  (Set  "("  ($#k3_tarski :::"Vertices"::: )  (Set (Var "G")) ")" )))) ; 
 
theorem :: SCMYCIEL:43 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "L")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "G"))  ($#k7_scmyciel :::"SubgraphInducedBy"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "G"))  ($#k7_scmyciel :::"SubgraphInducedBy"::: )  (Set  "(" (Set (Var "L"))  ($#k3_xboole_0 :::"/\"::: )  (Set  "("  ($#k3_tarski :::"Vertices"::: )  (Set (Var "G")) ")" ) ")" ))))) ; 
 registrationlet "G" be   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"SimpleGraph":::); let "L" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set "G"  ($#k7_scmyciel :::"SubgraphInducedBy"::: )  "L") ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; registrationlet "G" be   ($#m1_hidden :::"SimpleGraph":::); let "L" be   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster (Set "G"  ($#k7_scmyciel :::"SubgraphInducedBy"::: )  "L") ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; 
theorem :: SCMYCIEL:44 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#m1_hidden :::"SimpleGraph":::)  "st" (Bool (Bool (Set (Var "G"))  ($#r1_tarski :::"c="::: )  (Set (Var "H")))) "holds"  (Bool (Set (Var "G"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "H"))  ($#k7_scmyciel :::"SubgraphInducedBy"::: )  (Set  "("  ($#k3_tarski :::"Vertices"::: )  (Set (Var "G")) ")" )))) ; 
 
theorem :: SCMYCIEL:45 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "L")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k3_tarski :::"Vertices"::: )  (Set  "(" (Set (Var "G"))  ($#k7_scmyciel :::"SubgraphInducedBy"::: )  (Set (Var "L")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_tarski :::"Vertices"::: )  (Set (Var "G")) ")" )  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "L")))))) ; 
 
theorem :: SCMYCIEL:46 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "G"))))) "holds"  (Bool (Set (Set (Var "G"))  ($#k7_scmyciel :::"SubgraphInducedBy"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ($#k2_tarski :::"}"::: ) )))) ; 
 begin  definitionlet "G" be   ($#m1_hidden :::"SimpleGraph":::); attr "G" is  :::"clique":::  means :: SCMYCIEL:def 13 (Bool "G"  ($#r1_hidden :::"="::: )  (Set   ($#k5_scmyciel :::"CompleteSGraph"::: )  (Set  "("  ($#k3_tarski :::"Vertices"::: )  "G" ")" ))); end; 




:: deftheorem    defines :::"clique"::: SCMYCIEL:def 13 :  (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::) "holds"   (Bool  "("  (Bool (Set (Var "G")) "is"   ($#v5_scmyciel :::"clique"::: )  ) "iff" (Bool (Set (Var "G"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_scmyciel :::"CompleteSGraph"::: )  (Set  "("  ($#k3_tarski :::"Vertices"::: )  (Set (Var "G")) ")" )))  ")" )); 
 
theorem :: SCMYCIEL:47 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y"))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "G")))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "G"))))) "holds"  (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k1_scmyciel :::"Edges"::: )  (Set (Var "G"))))  ")" )) "holds"  (Bool (Set (Var "G")) "is"   ($#v5_scmyciel :::"clique"::: )  )) ; 
 
theorem :: SCMYCIEL:48 (Bool (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) "is"   ($#v5_scmyciel :::"clique"::: )  ) ; 
 registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v5_finset_1 :::"finite-membered"::: )   bbbadV2_FINSUB_1() bbbadV1_SETFAM_1()   ($#v1_classes1 :::"subset-closed"::: )   (Num 1)  ($#v3_scmyciel :::"-at_most_dimensional"::: )     ($#v4_scmyciel :::"SimpleGraph-like"::: )     ($#v5_scmyciel :::"clique"::: )    for    ($#m1_hidden :::"set"::: )  ; 
let "G" be   ($#m1_hidden :::"SimpleGraph":::); 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v5_finset_1 :::"finite-membered"::: )   bbbadV2_FINSUB_1() bbbadV1_SETFAM_1()   ($#v1_classes1 :::"subset-closed"::: )   (Num 1)  ($#v3_scmyciel :::"-at_most_dimensional"::: )     ($#v4_scmyciel :::"SimpleGraph-like"::: )     ($#v5_scmyciel :::"clique"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  "G"); 
end; definitionlet "G" be   ($#m1_hidden :::"SimpleGraph":::); mode Clique of "G" is   ($#v5_scmyciel :::"clique"::: )    ($#m1_subset_1 :::"Subgraph":::) "of" "G"; end; 
theorem :: SCMYCIEL:49 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k5_scmyciel :::"CompleteSGraph"::: )  (Set (Var "X"))) "is"   ($#v5_scmyciel :::"clique"::: )  )) ; 
 registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k5_scmyciel :::"CompleteSGraph"::: )  "X") ->   ($#v5_scmyciel :::"clique"::: )   ; 
end; 
theorem :: SCMYCIEL:50 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "G"))))) "holds"  (Bool (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ($#k2_tarski :::"}"::: ) ) "is"   ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "G"))))) ; 
 
theorem :: SCMYCIEL:51 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "G")))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "G")))) & (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "G")))) "holds"  (Bool (Set  ($#k2_enumset1 :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) "," (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ) ($#k2_enumset1 :::"}"::: ) ) "is"   ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "G"))))) ; 
 registrationlet "G" be   ($#m1_hidden :::"SimpleGraph":::); 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )     ($#v5_finset_1 :::"finite-membered"::: )   bbbadV2_FINSUB_1() bbbadV1_SETFAM_1()   ($#v1_classes1 :::"subset-closed"::: )   (Num 1)  ($#v3_scmyciel :::"-at_most_dimensional"::: )     ($#v4_scmyciel :::"SimpleGraph-like"::: )     ($#v5_scmyciel :::"clique"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  "G"); 
end; 
theorem :: SCMYCIEL:52 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "G"))))) "holds"  (Bool  "ex" (Set (Var "C")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "G")) "st" (Bool (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))))) ; 
 
theorem :: SCMYCIEL:53 (Bool  "for" (Set (Var "C")) "being"   ($#v5_scmyciel :::"clique"::: )    ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "u")) "," (Set (Var "v")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "u"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "C")))) & (Bool (Set (Var "v"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "C"))))) "holds"  (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "u")) "," (Set (Var "v")) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "C"))))) ; 
 definitionlet "G" be   ($#m1_hidden :::"SimpleGraph":::); attr "G" is  :::"with_finite_clique#":::  means :: SCMYCIEL:def 14 (Bool  "ex" (Set (Var "C")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Clique":::) "of" "G" "st"  (Bool  "for" (Set (Var "D")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Clique":::) "of" "G" "holds"  (Bool (Set   ($#k2_scmyciel :::"order"::: )  (Set (Var "D")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k2_scmyciel :::"order"::: )  (Set (Var "C")))))); end; 




:: deftheorem    defines :::"with_finite_clique#"::: SCMYCIEL:def 14 :  (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::) "holds"   (Bool  "("  (Bool (Set (Var "G")) "is"   ($#v6_scmyciel :::"with_finite_clique#"::: )  ) "iff" (Bool  "ex" (Set (Var "C")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "G")) "st"  (Bool  "for" (Set (Var "D")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "G")) "holds"  (Bool (Set   ($#k2_scmyciel :::"order"::: )  (Set (Var "D")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k2_scmyciel :::"order"::: )  (Set (Var "C"))))))  ")" )); 
 registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v5_finset_1 :::"finite-membered"::: )   bbbadV2_FINSUB_1() bbbadV1_SETFAM_1()   ($#v1_classes1 :::"subset-closed"::: )   (Num 1)  ($#v3_scmyciel :::"-at_most_dimensional"::: )     ($#v4_scmyciel :::"SimpleGraph-like"::: )     ($#v6_scmyciel :::"with_finite_clique#"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registration
cluster   ($#v1_finset_1 :::"finite"::: )     ($#v4_scmyciel :::"SimpleGraph-like"::: )    ->   ($#v6_scmyciel :::"with_finite_clique#"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; definitionlet "G" be   ($#v6_scmyciel :::"with_finite_clique#"::: )    ($#m1_hidden :::"SimpleGraph":::); func  :::"clique#"::: "G" ->   ($#m1_hidden :::"Nat":::) means :: SCMYCIEL:def 15 (Bool  "("  (Bool  "ex" (Set (Var "C")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Clique":::) "of" "G" "st" (Bool (Set   ($#k2_scmyciel :::"order"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  it)) & (Bool  "("   "for" (Set (Var "T")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Clique":::) "of" "G" "holds"  (Bool (Set   ($#k2_scmyciel :::"order"::: )  (Set (Var "T")))  ($#r1_xxreal_0 :::"<="::: )  it)  ")" )  ")" ); end; 





:: deftheorem    defines :::"clique#"::: SCMYCIEL:def 15 :  (Bool  "for" (Set (Var "G")) "being"   ($#v6_scmyciel :::"with_finite_clique#"::: )    ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_scmyciel :::"clique#"::: )  (Set (Var "G")))) "iff" (Bool  "("  (Bool  "ex" (Set (Var "C")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "G")) "st" (Bool (Set   ($#k2_scmyciel :::"order"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set (Var "b2")))) & (Bool  "("   "for" (Set (Var "T")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "G")) "holds"  (Bool (Set   ($#k2_scmyciel :::"order"::: )  (Set (Var "T")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b2")))  ")" )  ")" )  ")" ))); 
 
theorem :: SCMYCIEL:54 (Bool  "for" (Set (Var "G")) "being"   ($#v6_scmyciel :::"with_finite_clique#"::: )    ($#m1_hidden :::"SimpleGraph":::)  "st" (Bool (Bool (Set   ($#k8_scmyciel :::"clique#"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: SCMYCIEL:55 (Bool  "for" (Set (Var "G")) "being"   ($#v1_scmyciel :::"void"::: )    ($#m1_hidden :::"SimpleGraph":::) "holds"  (Bool (Set   ($#k8_scmyciel :::"clique#"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: SCMYCIEL:56 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "G")))) "holds"  (Bool (Set (Set (Var "G"))  ($#k7_scmyciel :::"SubgraphInducedBy"::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )) "is"   ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "G"))))) ; 
 
theorem :: SCMYCIEL:57 (Bool  "for" (Set (Var "G")) "being"   ($#v6_scmyciel :::"with_finite_clique#"::: )    ($#m1_hidden :::"SimpleGraph":::)  "st" (Bool (Bool (Set   ($#k1_scmyciel :::"Edges"::: )  (Set (Var "G")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set   ($#k8_scmyciel :::"clique#"::: )  (Set (Var "G")))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) ; 
 
theorem :: SCMYCIEL:58 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#v6_scmyciel :::"with_finite_clique#"::: )    ($#m1_hidden :::"SimpleGraph":::)  "st" (Bool (Bool (Set (Var "G"))  ($#r1_tarski :::"c="::: )  (Set (Var "H")))) "holds"  (Bool (Set   ($#k8_scmyciel :::"clique#"::: )  (Set (Var "G")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k8_scmyciel :::"clique#"::: )  (Set (Var "H"))))) ; 
 
theorem :: SCMYCIEL:59 (Bool  "for" (Set (Var "X")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k8_scmyciel :::"clique#"::: )  (Set  "("  ($#k5_scmyciel :::"CompleteSGraph"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "X"))))) ; 
 definitionlet "G" be   ($#m1_hidden :::"SimpleGraph":::); let "P" be    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Const "G"))); attr "P" is  :::"Clique-wise":::  means :: SCMYCIEL:def 16 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "P")) "holds"  (Bool (Set "G"  ($#k7_scmyciel :::"SubgraphInducedBy"::: )  (Set (Var "x"))) "is"   ($#m1_subset_1 :::"Clique":::) "of" "G")); end; 





:: deftheorem    defines :::"Clique-wise"::: SCMYCIEL:def 16 :  (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "P")) "being"    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "G"))) "holds"   (Bool  "("  (Bool (Set (Var "P")) "is"   ($#v7_scmyciel :::"Clique-wise"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "P")))) "holds"  (Bool (Set (Set (Var "G"))  ($#k7_scmyciel :::"SubgraphInducedBy"::: )  (Set (Var "x"))) "is"   ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "G"))))  ")" ))); 
 registrationlet "G" be   ($#m1_hidden :::"SimpleGraph":::); 
cluster bbbadV1_SETFAM_1()   ($#v7_scmyciel :::"Clique-wise"::: )    for    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set   ($#k3_tarski :::"Vertices"::: )  "G"); 
end; definitionlet "G" be   ($#m1_hidden :::"SimpleGraph":::); mode Clique-partition of "G" is   ($#v7_scmyciel :::"Clique-wise"::: )     ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set   ($#k3_tarski :::"Vertices"::: )  "G"); end; registrationlet "G" be   ($#v1_scmyciel :::"void"::: )    ($#m1_hidden :::"SimpleGraph":::); 
cluster   ($#v1_xboole_0 :::"empty"::: )    ->   ($#v7_scmyciel :::"Clique-wise"::: )    for    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set   ($#k3_tarski :::"Vertices"::: )  "G"); 
end; definitionlet "G" be   ($#m1_hidden :::"SimpleGraph":::); attr "G" is  :::"with_finite_cliquecover#":::  means :: SCMYCIEL:def 17 (Bool  "ex" (Set (Var "C")) "being"   ($#m1_eqrel_1 :::"Clique-partition":::) "of" "G" "st" (Bool (Set (Var "C")) "is"   ($#v1_finset_1 :::"finite"::: )  )); end; 




:: deftheorem    defines :::"with_finite_cliquecover#"::: SCMYCIEL:def 17 :  (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::) "holds"   (Bool  "("  (Bool (Set (Var "G")) "is"   ($#v8_scmyciel :::"with_finite_cliquecover#"::: )  ) "iff" (Bool  "ex" (Set (Var "C")) "being"   ($#m1_eqrel_1 :::"Clique-partition":::) "of" (Set (Var "G")) "st" (Bool (Set (Var "C")) "is"   ($#v1_finset_1 :::"finite"::: )  ))  ")" )); 
 registration
cluster   ($#v1_finset_1 :::"finite"::: )     ($#v4_scmyciel :::"SimpleGraph-like"::: )    ->   ($#v8_scmyciel :::"with_finite_cliquecover#"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "G" be   ($#v8_scmyciel :::"with_finite_cliquecover#"::: )    ($#m1_hidden :::"SimpleGraph":::); 
cluster   ($#v1_finset_1 :::"finite"::: )   bbbadV1_SETFAM_1()   ($#v7_scmyciel :::"Clique-wise"::: )    for    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set   ($#k3_tarski :::"Vertices"::: )  "G"); 
end; registrationlet "G" be   ($#v8_scmyciel :::"with_finite_cliquecover#"::: )    ($#m1_hidden :::"SimpleGraph":::); let "S" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_tarski :::"Vertices"::: )  (Set (Const "G")) ")" ); 
cluster (Set "G"  ($#k7_scmyciel :::"SubgraphInducedBy"::: )  "S") ->   ($#v8_scmyciel :::"with_finite_cliquecover#"::: )   ; 
end; definitionlet "G" be   ($#v8_scmyciel :::"with_finite_cliquecover#"::: )    ($#m1_hidden :::"SimpleGraph":::); func  :::"cliquecover#"::: "G" ->   ($#m1_hidden :::"Nat":::) means :: SCMYCIEL:def 18 (Bool  "("  (Bool  "ex" (Set (Var "C")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_eqrel_1 :::"Clique-partition":::) "of" "G" "st" (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  it)) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_eqrel_1 :::"Clique-partition":::) "of" "G" "holds"  (Bool it  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "C"))))  ")" )  ")" ); end; 





:: deftheorem    defines :::"cliquecover#"::: SCMYCIEL:def 18 :  (Bool  "for" (Set (Var "G")) "being"   ($#v8_scmyciel :::"with_finite_cliquecover#"::: )    ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k9_scmyciel :::"cliquecover#"::: )  (Set (Var "G")))) "iff" (Bool  "("  (Bool  "ex" (Set (Var "C")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_eqrel_1 :::"Clique-partition":::) "of" (Set (Var "G")) "st" (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set (Var "b2")))) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_eqrel_1 :::"Clique-partition":::) "of" (Set (Var "G")) "holds"  (Bool (Set (Var "b2"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "C"))))  ")" )  ")" )  ")" ))); 
 begin  definitionlet "G" be   ($#m1_hidden :::"SimpleGraph":::); let "S" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_tarski :::"Vertices"::: )  (Set (Const "G")) ")" ); attr "S" is  :::"stable":::  means :: SCMYCIEL:def 19 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y"))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "S") & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  "S")) "holds"  (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"nin"::: )  "G")); end; 





:: deftheorem    defines :::"stable"::: SCMYCIEL:def 19 :  (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_tarski :::"Vertices"::: )  (Set (Var "G")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v9_scmyciel :::"stable"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y"))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "S"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "S")))) "holds"  (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"nin"::: )  (Set (Var "G"))))  ")" ))); 
 
theorem :: SCMYCIEL:60 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::) "holds"  (Bool (Set   ($#k1_subset_1 :::"{}"::: )  (Set  "("  ($#k3_tarski :::"Vertices"::: )  (Set (Var "G")) ")" )) "is"   ($#v9_scmyciel :::"stable"::: )  )) ; 
 
theorem :: SCMYCIEL:61 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_tarski :::"Vertices"::: )  (Set (Var "G")) ")" )  (Bool  "for" (Set (Var "v")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "S"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "v")) ($#k1_tarski :::"}"::: ) ))) "holds"  (Bool (Set (Var "S")) "is"   ($#v9_scmyciel :::"stable"::: )  )))) ; 
 registrationlet "G" be   ($#m1_hidden :::"SimpleGraph":::); 
cluster   ($#v1_zfmisc_1 :::"trivial"::: )    ->   ($#v9_scmyciel :::"stable"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "("  ($#k3_tarski :::"Vertices"::: )  "G" ")" )); 
end; registrationlet "G" be   ($#m1_hidden :::"SimpleGraph":::); 
cluster   ($#v9_scmyciel :::"stable"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "("  ($#k3_tarski :::"Vertices"::: )  "G" ")" )); 
end; definitionlet "G" be   ($#m1_hidden :::"SimpleGraph":::); mode StableSet of "G" is   ($#v9_scmyciel :::"stable"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_tarski :::"Vertices"::: )  "G" ")" ); end; 
theorem :: SCMYCIEL:62 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "G")))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "G")))) & (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"nin"::: )  (Set (Var "G")))) "holds"  (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ) "is"   ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "G"))))) ; 
 
theorem :: SCMYCIEL:63 (Bool  "for" (Set (Var "G")) "being"   ($#v6_scmyciel :::"with_finite_clique#"::: )    ($#m1_hidden :::"SimpleGraph":::)  "st" (Bool (Bool (Set   ($#k8_scmyciel :::"clique#"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "G"))) "is"   ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "G")))) ; 
 registrationlet "G" be   ($#m1_hidden :::"SimpleGraph":::); 
cluster   ($#v1_finset_1 :::"finite"::: )     ($#v9_scmyciel :::"stable"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "("  ($#k3_tarski :::"Vertices"::: )  "G" ")" )); 
end; 
theorem :: SCMYCIEL:64 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds"  (Bool (Set (Var "B")) "is"   ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "G")))))) ; 
 definitionlet "G" be   ($#m1_hidden :::"SimpleGraph":::); let "P" be    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Const "G"))); attr "P" is  :::"StableSet-wise":::  means :: SCMYCIEL:def 20 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "P")) "holds"  (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"StableSet":::) "of" "G")); end; 





:: deftheorem    defines :::"StableSet-wise"::: SCMYCIEL:def 20 :  (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "P")) "being"    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "G"))) "holds"   (Bool  "("  (Bool (Set (Var "P")) "is"   ($#v10_scmyciel :::"StableSet-wise"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "P")))) "holds"  (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "G"))))  ")" ))); 
 
theorem :: SCMYCIEL:65 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::) "holds"  (Bool (Set   ($#k10_eqrel_1 :::"SmallestPartition"::: )  (Set  "("  ($#k3_tarski :::"Vertices"::: )  (Set (Var "G")) ")" )) "is"   ($#v10_scmyciel :::"StableSet-wise"::: )  )) ; 
 registrationlet "G" be   ($#m1_hidden :::"SimpleGraph":::); 
cluster bbbadV1_SETFAM_1()   ($#v10_scmyciel :::"StableSet-wise"::: )    for    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set   ($#k3_tarski :::"Vertices"::: )  "G"); 
end; definitionlet "G" be   ($#m1_hidden :::"SimpleGraph":::); mode Coloring of "G" is   ($#v10_scmyciel :::"StableSet-wise"::: )     ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set   ($#k3_tarski :::"Vertices"::: )  "G"); end; definitionlet "G" be   ($#m1_hidden :::"SimpleGraph":::); attr "G" is  :::"finitely_colorable":::  means :: SCMYCIEL:def 21 (Bool  "ex" (Set (Var "C")) "being"   ($#m1_eqrel_1 :::"Coloring":::) "of" "G" "st" (Bool (Set (Var "C")) "is"   ($#v1_finset_1 :::"finite"::: )  )); end; 




:: deftheorem    defines :::"finitely_colorable"::: SCMYCIEL:def 21 :  (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::) "holds"   (Bool  "("  (Bool (Set (Var "G")) "is"   ($#v11_scmyciel :::"finitely_colorable"::: )  ) "iff" (Bool  "ex" (Set (Var "C")) "being"   ($#m1_eqrel_1 :::"Coloring":::) "of" (Set (Var "G")) "st" (Bool (Set (Var "C")) "is"   ($#v1_finset_1 :::"finite"::: )  ))  ")" )); 
 registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v5_finset_1 :::"finite-membered"::: )   bbbadV2_FINSUB_1() bbbadV1_SETFAM_1()   ($#v1_classes1 :::"subset-closed"::: )   (Num 1)  ($#v3_scmyciel :::"-at_most_dimensional"::: )     ($#v4_scmyciel :::"SimpleGraph-like"::: )     ($#v11_scmyciel :::"finitely_colorable"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registration
cluster   ($#v1_finset_1 :::"finite"::: )     ($#v4_scmyciel :::"SimpleGraph-like"::: )    ->   ($#v11_scmyciel :::"finitely_colorable"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "G" be   ($#v11_scmyciel :::"finitely_colorable"::: )    ($#m1_hidden :::"SimpleGraph":::); 
cluster   ($#v1_finset_1 :::"finite"::: )   bbbadV1_SETFAM_1()   ($#v10_scmyciel :::"StableSet-wise"::: )    for    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set   ($#k3_tarski :::"Vertices"::: )  "G"); 
end; 
theorem :: SCMYCIEL:66 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "L")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "L"))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "S"))))) "holds"  (Bool (Set (Set (Var "G"))  ($#k7_scmyciel :::"SubgraphInducedBy"::: )  (Set (Var "L"))) "is"   ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "G")))))) ; 
 
theorem :: SCMYCIEL:67 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "C")) "being"   ($#m1_eqrel_1 :::"Coloring":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_tarski :::"Vertices"::: )  (Set (Var "G")) ")" ) "holds"  (Bool (Set (Set (Var "C"))  ($#k1_mycielsk :::"|"::: )  (Set (Var "S"))) "is"   ($#m1_eqrel_1 :::"Coloring":::) "of" (Set  "(" (Set (Var "G"))  ($#k7_scmyciel :::"SubgraphInducedBy"::: )  (Set (Var "S")) ")" ))))) ; 
 registrationlet "G" be   ($#v11_scmyciel :::"finitely_colorable"::: )    ($#m1_hidden :::"SimpleGraph":::); let "S" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set "G"  ($#k7_scmyciel :::"SubgraphInducedBy"::: )  "S") ->   ($#v11_scmyciel :::"finitely_colorable"::: )   ; 
end; definitionlet "G" be   ($#v11_scmyciel :::"finitely_colorable"::: )    ($#m1_hidden :::"SimpleGraph":::); func  :::"chromatic#"::: "G" ->   ($#m1_hidden :::"Nat":::) means :: SCMYCIEL:def 22 (Bool  "("  (Bool  "ex" (Set (Var "C")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_eqrel_1 :::"Coloring":::) "of" "G" "st" (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  it)) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_eqrel_1 :::"Coloring":::) "of" "G" "holds"  (Bool it  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "C"))))  ")" )  ")" ); end; 





:: deftheorem    defines :::"chromatic#"::: SCMYCIEL:def 22 :  (Bool  "for" (Set (Var "G")) "being"   ($#v11_scmyciel :::"finitely_colorable"::: )    ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_scmyciel :::"chromatic#"::: )  (Set (Var "G")))) "iff" (Bool  "("  (Bool  "ex" (Set (Var "C")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_eqrel_1 :::"Coloring":::) "of" (Set (Var "G")) "st" (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set (Var "b2")))) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_eqrel_1 :::"Coloring":::) "of" (Set (Var "G")) "holds"  (Bool (Set (Var "b2"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "C"))))  ")" )  ")" )  ")" ))); 
 
theorem :: SCMYCIEL:68 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#v11_scmyciel :::"finitely_colorable"::: )    ($#m1_hidden :::"SimpleGraph":::)  "st" (Bool (Bool (Set (Var "G"))  ($#r1_tarski :::"c="::: )  (Set (Var "H")))) "holds"  (Bool (Set   ($#k10_scmyciel :::"chromatic#"::: )  (Set (Var "G")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k10_scmyciel :::"chromatic#"::: )  (Set (Var "H"))))) ; 
 
theorem :: SCMYCIEL:69 (Bool  "for" (Set (Var "X")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k10_scmyciel :::"chromatic#"::: )  (Set  "("  ($#k5_scmyciel :::"CompleteSGraph"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "X"))))) ; 
 
theorem :: SCMYCIEL:70 (Bool  "for" (Set (Var "G")) "being"   ($#v11_scmyciel :::"finitely_colorable"::: )    ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "C")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_eqrel_1 :::"Coloring":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "c")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set   ($#k10_scmyciel :::"chromatic#"::: )  (Set (Var "G"))))) "holds"  (Bool  "ex" (Set (Var "v")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "G"))) "st"  (Bool  "("  (Bool (Set (Var "v"))  ($#r2_hidden :::"in"::: )  (Set (Var "c"))) & (Bool  "("   "for" (Set (Var "d")) "being"    ($#m1_card_lar :::"Element"::: )   "of" (Set (Var "C"))  "st" (Bool (Bool (Set (Var "d"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c")))) "holds"  (Bool  "ex" (Set (Var "w")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "G"))) "st"  (Bool  "("  (Bool (Set (Var "w"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_scmyciel :::"Adjacent"::: )  (Set (Var "v")))) & (Bool (Set (Var "w"))  ($#r2_hidden :::"in"::: )  (Set (Var "d")))  ")" ))  ")" )  ")" ))))) ; 
 definitionlet "G" be   ($#m1_hidden :::"SimpleGraph":::); attr "G" is  :::"with_finite_stability#":::  means :: SCMYCIEL:def 23 (Bool  "ex" (Set (Var "A")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"StableSet":::) "of" "G" "st"  (Bool  "for" (Set (Var "B")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"StableSet":::) "of" "G" "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "B")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "A")))))); end; 




:: deftheorem    defines :::"with_finite_stability#"::: SCMYCIEL:def 23 :  (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::) "holds"   (Bool  "("  (Bool (Set (Var "G")) "is"   ($#v12_scmyciel :::"with_finite_stability#"::: )  ) "iff" (Bool  "ex" (Set (Var "A")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "G")) "st"  (Bool  "for" (Set (Var "B")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "G")) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "B")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "A"))))))  ")" )); 
 registration
cluster   ($#v1_finset_1 :::"finite"::: )     ($#v4_scmyciel :::"SimpleGraph-like"::: )    ->   ($#v12_scmyciel :::"with_finite_stability#"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "G" be   ($#v12_scmyciel :::"with_finite_stability#"::: )    ($#m1_hidden :::"SimpleGraph":::); 
cluster   ($#v9_scmyciel :::"stable"::: )    ->   ($#v1_finset_1 :::"finite"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "("  ($#k3_tarski :::"Vertices"::: )  "G" ")" )); 
end; registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v5_finset_1 :::"finite-membered"::: )   bbbadV2_FINSUB_1() bbbadV1_SETFAM_1()   ($#v1_classes1 :::"subset-closed"::: )    ($#~v1_scmyciel  "non"   ($#v1_scmyciel :::"void"::: )   )  (Num 1)  ($#v3_scmyciel :::"-at_most_dimensional"::: )     ($#v4_scmyciel :::"SimpleGraph-like"::: )     ($#v12_scmyciel :::"with_finite_stability#"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; definitionlet "G" be   ($#v12_scmyciel :::"with_finite_stability#"::: )    ($#m1_hidden :::"SimpleGraph":::); func  :::"stability#"::: "G" ->   ($#m1_hidden :::"Nat":::) means :: SCMYCIEL:def 24 (Bool  "("  (Bool  "ex" (Set (Var "A")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"StableSet":::) "of" "G" "st" (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  it)) & (Bool  "("   "for" (Set (Var "T")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"StableSet":::) "of" "G" "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "T")))  ($#r1_xxreal_0 :::"<="::: )  it)  ")" )  ")" ); end; 





:: deftheorem    defines :::"stability#"::: SCMYCIEL:def 24 :  (Bool  "for" (Set (Var "G")) "being"   ($#v12_scmyciel :::"with_finite_stability#"::: )    ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_scmyciel :::"stability#"::: )  (Set (Var "G")))) "iff" (Bool  "("  (Bool  "ex" (Set (Var "A")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "G")) "st" (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "b2")))) & (Bool  "("   "for" (Set (Var "T")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "G")) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "T")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b2")))  ")" )  ")" )  ")" ))); 
 registrationlet "G" be  ($#~v1_scmyciel  "non"   ($#v1_scmyciel :::"void"::: )   )    ($#v12_scmyciel :::"with_finite_stability#"::: )    ($#m1_hidden :::"SimpleGraph":::); 
cluster (Set   ($#k11_scmyciel :::"stability#"::: )  "G") ->   ($#v2_xxreal_0 :::"positive"::: )   ; 
end; 
theorem :: SCMYCIEL:71 (Bool  "for" (Set (Var "G")) "being"   ($#v12_scmyciel :::"with_finite_stability#"::: )    ($#m1_hidden :::"SimpleGraph":::)  "st" (Bool (Bool (Set   ($#k11_scmyciel :::"stability#"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set (Var "G")) "is"   ($#v5_scmyciel :::"clique"::: )  )) ; 
 registration
cluster   ($#v4_scmyciel :::"SimpleGraph-like"::: )     ($#v6_scmyciel :::"with_finite_clique#"::: )     ($#v12_scmyciel :::"with_finite_stability#"::: )    ->   ($#v1_finset_1 :::"finite"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: SCMYCIEL:72 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "G")) "holds"  (Bool (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "C"))) "is"   ($#m1_subset_1 :::"StableSet":::) "of" (Set  "("  ($#k6_scmyciel :::"Complement"::: )  (Set (Var "G")) ")" )))) ; 
 
theorem :: SCMYCIEL:73 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Clique":::) "of" (Set  "("  ($#k6_scmyciel :::"Complement"::: )  (Set (Var "G")) ")" ) "holds"  (Bool (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "C"))) "is"   ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "G"))))) ; 
 
theorem :: SCMYCIEL:74 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "G")) "holds"  (Bool (Set (Set  "("  ($#k6_scmyciel :::"Complement"::: )  (Set (Var "G")) ")" )  ($#k7_scmyciel :::"SubgraphInducedBy"::: )  (Set (Var "C"))) "is"   ($#m1_subset_1 :::"Clique":::) "of" (Set  "("  ($#k6_scmyciel :::"Complement"::: )  (Set (Var "G")) ")" )))) ; 
 
theorem :: SCMYCIEL:75 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"StableSet":::) "of" (Set  "("  ($#k6_scmyciel :::"Complement"::: )  (Set (Var "G")) ")" ) "holds"  (Bool (Set (Set (Var "G"))  ($#k7_scmyciel :::"SubgraphInducedBy"::: )  (Set (Var "C"))) "is"   ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "G"))))) ; 
 registrationlet "G" be   ($#v6_scmyciel :::"with_finite_clique#"::: )    ($#m1_hidden :::"SimpleGraph":::); 
cluster (Set   ($#k6_scmyciel :::"Complement"::: )  "G") ->   ($#v12_scmyciel :::"with_finite_stability#"::: )   ; 
end; registrationlet "G" be   ($#v12_scmyciel :::"with_finite_stability#"::: )    ($#m1_hidden :::"SimpleGraph":::); 
cluster (Set   ($#k6_scmyciel :::"Complement"::: )  "G") ->   ($#v6_scmyciel :::"with_finite_clique#"::: )   ; 
end; 
theorem :: SCMYCIEL:76 (Bool  "for" (Set (Var "G")) "being"   ($#v6_scmyciel :::"with_finite_clique#"::: )    ($#m1_hidden :::"SimpleGraph":::) "holds"  (Bool (Set   ($#k8_scmyciel :::"clique#"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set   ($#k11_scmyciel :::"stability#"::: )  (Set  "("  ($#k6_scmyciel :::"Complement"::: )  (Set (Var "G")) ")" )))) ; 
 
theorem :: SCMYCIEL:77 (Bool  "for" (Set (Var "G")) "being"   ($#v12_scmyciel :::"with_finite_stability#"::: )    ($#m1_hidden :::"SimpleGraph":::) "holds"  (Bool (Set   ($#k11_scmyciel :::"stability#"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set   ($#k8_scmyciel :::"clique#"::: )  (Set  "("  ($#k6_scmyciel :::"Complement"::: )  (Set (Var "G")) ")" )))) ; 
 
theorem :: SCMYCIEL:78 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "C")) "being"   ($#m1_eqrel_1 :::"Clique-partition":::) "of" (Set  "("  ($#k6_scmyciel :::"Complement"::: )  (Set (Var "G")) ")" ) "holds"  (Bool (Set (Var "C")) "is"   ($#m1_eqrel_1 :::"Coloring":::) "of" (Set (Var "G"))))) ; 
 
theorem :: SCMYCIEL:79 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "C")) "being"   ($#m1_eqrel_1 :::"Clique-partition":::) "of" (Set (Var "G")) "holds"  (Bool (Set (Var "C")) "is"   ($#m1_eqrel_1 :::"Coloring":::) "of" (Set  "("  ($#k6_scmyciel :::"Complement"::: )  (Set (Var "G")) ")" )))) ; 
 
theorem :: SCMYCIEL:80 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "C")) "being"   ($#m1_eqrel_1 :::"Coloring":::) "of" (Set (Var "G")) "holds"  (Bool (Set (Var "C")) "is"   ($#m1_eqrel_1 :::"Clique-partition":::) "of" (Set  "("  ($#k6_scmyciel :::"Complement"::: )  (Set (Var "G")) ")" )))) ; 
 
theorem :: SCMYCIEL:81 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "C")) "being"   ($#m1_eqrel_1 :::"Coloring":::) "of" (Set  "("  ($#k6_scmyciel :::"Complement"::: )  (Set (Var "G")) ")" ) "holds"  (Bool (Set (Var "C")) "is"   ($#m1_eqrel_1 :::"Clique-partition":::) "of" (Set (Var "G"))))) ; 
 registrationlet "G" be   ($#v11_scmyciel :::"finitely_colorable"::: )    ($#m1_hidden :::"SimpleGraph":::); 
cluster (Set   ($#k6_scmyciel :::"Complement"::: )  "G") ->   ($#v8_scmyciel :::"with_finite_cliquecover#"::: )   ; 
end; registrationlet "G" be   ($#v8_scmyciel :::"with_finite_cliquecover#"::: )    ($#m1_hidden :::"SimpleGraph":::); 
cluster (Set   ($#k6_scmyciel :::"Complement"::: )  "G") ->   ($#v11_scmyciel :::"finitely_colorable"::: )   ; 
end; 
theorem :: SCMYCIEL:82 (Bool  "for" (Set (Var "G")) "being"   ($#v11_scmyciel :::"finitely_colorable"::: )    ($#m1_hidden :::"SimpleGraph":::) "holds"  (Bool (Set   ($#k10_scmyciel :::"chromatic#"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set   ($#k9_scmyciel :::"cliquecover#"::: )  (Set  "("  ($#k6_scmyciel :::"Complement"::: )  (Set (Var "G")) ")" )))) ; 
 
theorem :: SCMYCIEL:83 (Bool  "for" (Set (Var "G")) "being"   ($#v8_scmyciel :::"with_finite_cliquecover#"::: )    ($#m1_hidden :::"SimpleGraph":::) "holds"  (Bool (Set   ($#k9_scmyciel :::"cliquecover#"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set   ($#k10_scmyciel :::"chromatic#"::: )  (Set  "("  ($#k6_scmyciel :::"Complement"::: )  (Set (Var "G")) ")" )))) ; 
 begin  definitionlet "G" be   ($#m1_hidden :::"SimpleGraph":::); func  :::"Mycielskian"::: "G" ->   ($#m1_hidden :::"SimpleGraph":::) equals :: SCMYCIEL:def 25 (Set (Set  "(" (Set  "(" (Set  "(" (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )  ($#k2_xboole_0 :::"\/"::: )   "{"  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) where x "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Set  "(" (Set  "("  ($#k3_tarski :::"union"::: )  "G" ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k3_tarski :::"union"::: )  "G" ")" ) "," (Set  ($#k1_tarski :::"{"::: ) (Set  "("  ($#k3_tarski :::"union"::: )  "G" ")" ) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "("  ($#k3_tarski :::"union"::: )  "G" ")" ) ($#k1_tarski :::"}"::: ) )) : (Bool verum)  "}"   ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "("  ($#k1_scmyciel :::"Edges"::: )  "G" ")" ) ")" )  ($#k2_xboole_0 :::"\/"::: )   "{"  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set  "("  ($#k3_tarski :::"union"::: )  "G" ")" ) ($#k4_tarski :::"]"::: ) ) ($#k2_tarski :::"}"::: ) ) where x, y "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k3_tarski :::"union"::: )  "G") : (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k1_scmyciel :::"Edges"::: )  "G"))  "}"   ")" )  ($#k2_xboole_0 :::"\/"::: )   "{"  (Set  ($#k2_tarski :::"{"::: ) (Set  "("  ($#k3_tarski :::"union"::: )  "G" ")" ) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set  "("  ($#k3_tarski :::"union"::: )  "G" ")" ) ($#k4_tarski :::"]"::: ) ) ($#k2_tarski :::"}"::: ) ) where x "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k3_tarski :::"union"::: )  "G") : (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"Vertices"::: )  "G"))  "}"  ); end; 





:: deftheorem    defines :::"Mycielskian"::: SCMYCIEL:def 25 :  (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::) "holds"  (Bool (Set   ($#k12_scmyciel :::"Mycielskian"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )  ($#k2_xboole_0 :::"\/"::: )   "{"  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) where x "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Set  "(" (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" ) "," (Set  ($#k1_tarski :::"{"::: ) (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" ) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" ) ($#k1_tarski :::"}"::: ) )) : (Bool verum)  "}"   ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "("  ($#k1_scmyciel :::"Edges"::: )  (Set (Var "G")) ")" ) ")" )  ($#k2_xboole_0 :::"\/"::: )   "{"  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#k2_tarski :::"}"::: ) ) where x, y "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k3_tarski :::"union"::: )  (Set (Var "G"))) : (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k1_scmyciel :::"Edges"::: )  (Set (Var "G"))))  "}"   ")" )  ($#k2_xboole_0 :::"\/"::: )   "{"  (Set  ($#k2_tarski :::"{"::: ) (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" ) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#k2_tarski :::"}"::: ) ) where x "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k3_tarski :::"union"::: )  (Set (Var "G"))) : (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "G"))))  "}"  ))); 
 
theorem :: SCMYCIEL:84 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::) "holds"  (Bool (Set (Var "G"))  ($#r1_tarski :::"c="::: )  (Set   ($#k12_scmyciel :::"Mycielskian"::: )  (Set (Var "G"))))) ; 
 
theorem :: SCMYCIEL:85 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "v")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "v"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"Vertices"::: )  (Set  "("  ($#k12_scmyciel :::"Mycielskian"::: )  (Set (Var "G")) ")" ))) "iff" (Bool  "("  (Bool (Set (Var "v"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "G")))) "or" (Bool  "ex" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "G")))) & (Bool (Set (Var "v"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" ) ($#k4_tarski :::"]"::: ) ))  ")" )) "or" (Bool (Set (Var "v"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "G"))))  ")" )  ")" ))) ; 
 
theorem :: SCMYCIEL:86 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::) "holds"  (Bool (Set   ($#k3_tarski :::"Vertices"::: )  (Set  "("  ($#k12_scmyciel :::"Mycielskian"::: )  (Set (Var "G")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" ) "," (Set  ($#k1_tarski :::"{"::: ) (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" ) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" ) ($#k1_tarski :::"}"::: ) )))) ; 
 
theorem :: SCMYCIEL:87 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::) "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set (Var "G")))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"union"::: )  (Set  "("  ($#k12_scmyciel :::"Mycielskian"::: )  (Set (Var "G")) ")" )))) ; 
 
theorem :: SCMYCIEL:88 (Bool  "for" (Set (Var "G")) "being"   ($#v1_scmyciel :::"void"::: )    ($#m1_hidden :::"SimpleGraph":::) "holds"  (Bool (Set   ($#k12_scmyciel :::"Mycielskian"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) "," (Set  ($#k1_tarski :::"{"::: ) (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" ) ($#k1_tarski :::"}"::: ) ) ($#k2_tarski :::"}"::: ) ))) ; 
 registrationlet "G" be   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"SimpleGraph":::); 
cluster (Set   ($#k12_scmyciel :::"Mycielskian"::: )  "G") ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; 
theorem :: SCMYCIEL:89 (Bool  "for" (Set (Var "G")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"SimpleGraph":::) "holds"  (Bool (Set   ($#k2_scmyciel :::"order"::: )  (Set  "("  ($#k12_scmyciel :::"Mycielskian"::: )  (Set (Var "G")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set  "("  ($#k2_scmyciel :::"order"::: )  (Set (Var "G")) ")" ) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1)))) ; 
 
theorem :: SCMYCIEL:90 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "e")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_scmyciel :::"Edges"::: )  (Set  "("  ($#k12_scmyciel :::"Mycielskian"::: )  (Set (Var "G")) ")" ))) "iff" (Bool  "("  (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_scmyciel :::"Edges"::: )  (Set (Var "G")))) "or" (Bool  "ex" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k3_tarski :::"union"::: )  (Set (Var "G"))) "st"  (Bool  "("  (Bool (Set (Var "e"))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#k2_tarski :::"}"::: ) )) & (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k1_scmyciel :::"Edges"::: )  (Set (Var "G"))))  ")" )) "or" (Bool  "ex" (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k3_tarski :::"union"::: )  (Set (Var "G"))) "st"  (Bool  "("  (Bool (Set (Var "e"))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" ) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#k2_tarski :::"}"::: ) )) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "G"))))  ")" ))  ")" )  ")" ))) ; 
 
theorem :: SCMYCIEL:91 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::) "holds"  (Bool (Set   ($#k1_scmyciel :::"Edges"::: )  (Set  "("  ($#k12_scmyciel :::"Mycielskian"::: )  (Set (Var "G")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k1_scmyciel :::"Edges"::: )  (Set (Var "G")) ")" )  ($#k2_xboole_0 :::"\/"::: )   "{"  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#k2_tarski :::"}"::: ) ) where x, y "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k3_tarski :::"union"::: )  (Set (Var "G"))) : (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k1_scmyciel :::"Edges"::: )  (Set (Var "G"))))  "}"   ")" )  ($#k2_xboole_0 :::"\/"::: )   "{"  (Set  ($#k2_tarski :::"{"::: ) (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" ) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#k2_tarski :::"}"::: ) ) where y "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k3_tarski :::"union"::: )  (Set (Var "G"))) : (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "G"))))  "}"  ))) ; 
 
theorem :: SCMYCIEL:92 (Bool  "for" (Set (Var "G")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"SimpleGraph":::) "holds"  (Bool (Set   ($#k3_scmyciel :::"size"::: )  (Set  "("  ($#k12_scmyciel :::"Mycielskian"::: )  (Set (Var "G")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 3)  ($#k4_nat_1 :::"*"::: )  (Set  "("  ($#k3_scmyciel :::"size"::: )  (Set (Var "G")) ")" ) ")" )  ($#k2_nat_1 :::"+"::: )  (Set  "("  ($#k2_scmyciel :::"order"::: )  (Set (Var "G")) ")" )))) ; 
 
theorem :: SCMYCIEL:93 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "s")) "," (Set (Var "t")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "("   "not" (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k1_scmyciel :::"Edges"::: )  (Set  "("  ($#k12_scmyciel :::"Mycielskian"::: )  (Set (Var "G")) ")" ))) "or" (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k1_scmyciel :::"Edges"::: )  (Set (Var "G")))) "or" (Bool  "("  (Bool  "("  (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "G")))) "or" (Bool (Set (Var "s"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "G"))))  ")" ) & (Bool  "ex" (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "G")))) & (Bool (Set (Var "t"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" ) ($#k4_tarski :::"]"::: ) ))  ")" ))  ")" ) "or" (Bool  "("  (Bool  "("  (Bool (Set (Var "t"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "G")))) "or" (Bool (Set (Var "t"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "G"))))  ")" ) & (Bool  "ex" (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "G")))) & (Bool (Set (Var "s"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" ) ($#k4_tarski :::"]"::: ) ))  ")" ))  ")" )  ")" ))) ; 
 
theorem :: SCMYCIEL:94 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "u")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set  ($#k2_tarski :::"{"::: ) (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" ) "," (Set (Var "u")) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k1_scmyciel :::"Edges"::: )  (Set  "("  ($#k12_scmyciel :::"Mycielskian"::: )  (Set (Var "G")) ")" )))) "holds"  (Bool  "ex" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "G")))) & (Bool (Set (Var "u"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" ) ($#k4_tarski :::"]"::: ) ))  ")" )))) ; 
 
theorem :: SCMYCIEL:95 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "u")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "u"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "G"))))) "holds"  (Bool (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "u")) "," (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k12_scmyciel :::"Mycielskian"::: )  (Set (Var "G")))))) ; 
 
theorem :: SCMYCIEL:96 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "u")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "u"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "G"))))) "holds"  (Bool (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "u")) "," (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" ) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k12_scmyciel :::"Mycielskian"::: )  (Set (Var "G")))))) ; 
 
theorem :: SCMYCIEL:97 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "holds" (Bool (Bool  "not" (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k1_scmyciel :::"Edges"::: )  (Set  "("  ($#k12_scmyciel :::"Mycielskian"::: )  (Set (Var "G")) ")" )))))) ; 
 
theorem :: SCMYCIEL:98 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y")))) "holds"  (Bool  "not" (Bool (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k12_scmyciel :::"Mycielskian"::: )  (Set (Var "G"))))))) ; 
 
theorem :: SCMYCIEL:99 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k1_scmyciel :::"Edges"::: )  (Set  "("  ($#k12_scmyciel :::"Mycielskian"::: )  (Set (Var "G")) ")" )))) "holds"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y"))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "G")))) & (Bool  "("  (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "G")))) "or" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "G"))))  ")" )  ")" ))) ; 
 
theorem :: SCMYCIEL:100 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k12_scmyciel :::"Mycielskian"::: )  (Set (Var "G"))))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y"))))) ; 
 
theorem :: SCMYCIEL:101 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "G")))) & (Bool (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k12_scmyciel :::"Mycielskian"::: )  (Set (Var "G"))))) "holds"  (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "G"))))) ; 
 
theorem :: SCMYCIEL:102 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k1_scmyciel :::"Edges"::: )  (Set (Var "G"))))) "holds"  (Bool (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k12_scmyciel :::"Mycielskian"::: )  (Set (Var "G")))))) ; 
 
theorem :: SCMYCIEL:103 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "G")))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "G")))) & (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k12_scmyciel :::"Mycielskian"::: )  (Set (Var "G"))))) "holds"  (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "G"))))) ; 
 
theorem :: SCMYCIEL:104 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::) "holds"  (Bool (Set (Var "G"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k12_scmyciel :::"Mycielskian"::: )  (Set (Var "G")) ")" )  ($#k7_scmyciel :::"SubgraphInducedBy"::: )  (Set  "("  ($#k3_tarski :::"Vertices"::: )  (Set (Var "G")) ")" )))) ; 
 
theorem :: SCMYCIEL:105 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "C")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Clique":::) "of" (Set  "("  ($#k12_scmyciel :::"Mycielskian"::: )  (Set (Var "G")) ")" )  "st" (Bool (Bool (Num 3)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k2_scmyciel :::"order"::: )  (Set (Var "C"))))) "holds"  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "C"))  "holds" (Bool (Set (Var "v"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "G"))))))) ; 
 
theorem :: SCMYCIEL:106 (Bool  "for" (Set (Var "G")) "being"   ($#v6_scmyciel :::"with_finite_clique#"::: )    ($#m1_hidden :::"SimpleGraph":::)  "st" (Bool (Bool (Set   ($#k8_scmyciel :::"clique#"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "D")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Clique":::) "of" (Set  "("  ($#k12_scmyciel :::"Mycielskian"::: )  (Set (Var "G")) ")" ) "holds"  (Bool (Set   ($#k2_scmyciel :::"order"::: )  (Set (Var "D")))  ($#r1_xxreal_0 :::"<="::: )  (Num 1)))) ; 
 
theorem :: SCMYCIEL:107 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k3_tarski :::"Vertices"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) "holds"  (Bool (Set   ($#k12_scmyciel :::"Mycielskian"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set  ($#k3_enumset1 :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "," (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set  ($#k1_tarski :::"{"::: ) (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" ) ($#k1_tarski :::"}"::: ) ) "," (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "G")) ")" ) ($#k2_tarski :::"}"::: ) ) ($#k3_enumset1 :::"}"::: ) )))) ; 
 
theorem :: SCMYCIEL:108 (Bool  "for" (Set (Var "G")) "being"   ($#v6_scmyciel :::"with_finite_clique#"::: )    ($#m1_hidden :::"SimpleGraph":::)  "st" (Bool (Bool (Set   ($#k8_scmyciel :::"clique#"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool  "for" (Set (Var "D")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Clique":::) "of" (Set  "("  ($#k12_scmyciel :::"Mycielskian"::: )  (Set (Var "G")) ")" ) "holds"  (Bool (Set   ($#k2_scmyciel :::"order"::: )  (Set (Var "D")))  ($#r1_xxreal_0 :::"<="::: )  (Num 2)))) ; 
 
theorem :: SCMYCIEL:109 (Bool  "for" (Set (Var "G")) "being"   ($#v6_scmyciel :::"with_finite_clique#"::: )    ($#m1_hidden :::"SimpleGraph":::)  "st" (Bool (Bool (Num 2)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k8_scmyciel :::"clique#"::: )  (Set (Var "G"))))) "holds"  (Bool  "for" (Set (Var "D")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Clique":::) "of" (Set  "("  ($#k12_scmyciel :::"Mycielskian"::: )  (Set (Var "G")) ")" ) "holds"  (Bool (Set   ($#k2_scmyciel :::"order"::: )  (Set (Var "D")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k8_scmyciel :::"clique#"::: )  (Set (Var "G")))))) ; 
 registrationlet "G" be   ($#v6_scmyciel :::"with_finite_clique#"::: )    ($#m1_hidden :::"SimpleGraph":::); 
cluster (Set   ($#k12_scmyciel :::"Mycielskian"::: )  "G") ->   ($#v6_scmyciel :::"with_finite_clique#"::: )   ; 
end; 
theorem :: SCMYCIEL:110 (Bool  "for" (Set (Var "G")) "being"   ($#v6_scmyciel :::"with_finite_clique#"::: )    ($#m1_hidden :::"SimpleGraph":::)  "st" (Bool (Bool (Num 2)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k8_scmyciel :::"clique#"::: )  (Set (Var "G"))))) "holds"  (Bool (Set   ($#k8_scmyciel :::"clique#"::: )  (Set  "("  ($#k12_scmyciel :::"Mycielskian"::: )  (Set (Var "G")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k8_scmyciel :::"clique#"::: )  (Set (Var "G"))))) ; 
 
theorem :: SCMYCIEL:111 (Bool  "for" (Set (Var "G")) "being"   ($#v11_scmyciel :::"finitely_colorable"::: )    ($#m1_hidden :::"SimpleGraph":::) (Bool  "ex" (Set (Var "E")) "being"   ($#m1_eqrel_1 :::"Coloring":::) "of" (Set  "("  ($#k12_scmyciel :::"Mycielskian"::: )  (Set (Var "G")) ")" ) "st" (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "E")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k2_nat_1 :::"+"::: )  (Set  "("  ($#k10_scmyciel :::"chromatic#"::: )  (Set (Var "G")) ")" ))))) ; 
 registrationlet "G" be   ($#v11_scmyciel :::"finitely_colorable"::: )    ($#m1_hidden :::"SimpleGraph":::); 
cluster (Set   ($#k12_scmyciel :::"Mycielskian"::: )  "G") ->   ($#v11_scmyciel :::"finitely_colorable"::: )   ; 
end; 
theorem :: SCMYCIEL:112 (Bool  "for" (Set (Var "G")) "being"   ($#v11_scmyciel :::"finitely_colorable"::: )    ($#m1_hidden :::"SimpleGraph":::) "holds"  (Bool (Set   ($#k10_scmyciel :::"chromatic#"::: )  (Set  "("  ($#k12_scmyciel :::"Mycielskian"::: )  (Set (Var "G")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k2_nat_1 :::"+"::: )  (Set  "("  ($#k10_scmyciel :::"chromatic#"::: )  (Set (Var "G")) ")" )))) ; 
 definitionlet "G" be   ($#m1_hidden :::"SimpleGraph":::); func  :::"MycielskianSeq"::: "G" ->   ($#m1_hidden :::"ManySortedSet":::) "of" (Set   ($#k5_numbers :::"NAT"::: )  ) means :: SCMYCIEL:def 26 (Bool  "ex" (Set (Var "myc")) "being"   ($#m1_hidden :::"Function":::) "st"  (Bool  "("  (Bool it  ($#r1_hidden :::"="::: )  (Set (Var "myc"))) & (Bool (Set (Set (Var "myc"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  "G") & (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  "st" (Bool (Bool (Set (Var "G"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "myc"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k"))))) "holds"  (Bool (Set (Set (Var "myc"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k12_scmyciel :::"Mycielskian"::: )  (Set (Var "G")))))  ")" )  ")" )); end; 





:: deftheorem    defines :::"MycielskianSeq"::: SCMYCIEL:def 26 :  (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k13_scmyciel :::"MycielskianSeq"::: )  (Set (Var "G")))) "iff" (Bool  "ex" (Set (Var "myc")) "being"   ($#m1_hidden :::"Function":::) "st"  (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set (Var "myc"))) & (Bool (Set (Set (Var "myc"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "G"))) & (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  "st" (Bool (Bool (Set (Var "G"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "myc"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k"))))) "holds"  (Bool (Set (Set (Var "myc"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k12_scmyciel :::"Mycielskian"::: )  (Set (Var "G")))))  ")" )  ")" ))  ")" ))); 
 
theorem :: SCMYCIEL:113 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::) "holds"  (Bool (Set (Set  "("  ($#k13_scmyciel :::"MycielskianSeq"::: )  (Set (Var "G")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "G")))) ; 
 
theorem :: SCMYCIEL:114 (Bool  "for" (Set (Var "G")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "("  ($#k13_scmyciel :::"MycielskianSeq"::: )  (Set (Var "G")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "n"))) "is"   ($#m1_hidden :::"SimpleGraph":::)))) ; 
 registrationlet "G" be   ($#m1_hidden :::"SimpleGraph":::); let "n" be   ($#m1_hidden :::"Nat":::); 
cluster (Set (Set  "("  ($#k13_scmyciel :::"MycielskianSeq"::: )  "G" ")" )  ($#k1_funct_1 :::"."::: )  "n") ->   ($#v4_scmyciel :::"SimpleGraph-like"::: )   ; 
end; 
theorem :: SCMYCIEL:115 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "("  ($#k13_scmyciel :::"MycielskianSeq"::: )  (Set (Var "G")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k12_scmyciel :::"Mycielskian"::: )  (Set  "(" (Set  "("  ($#k13_scmyciel :::"MycielskianSeq"::: )  (Set (Var "G")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "n")) ")" ))))) ; 
 registrationlet "G" be   ($#v6_scmyciel :::"with_finite_clique#"::: )    ($#m1_hidden :::"SimpleGraph":::); let "n" be   ($#m1_hidden :::"Nat":::); 
cluster (Set (Set  "("  ($#k13_scmyciel :::"MycielskianSeq"::: )  "G" ")" )  ($#k1_funct_1 :::"."::: )  "n") ->   ($#v6_scmyciel :::"with_finite_clique#"::: )   ; 
end; registrationlet "G" be   ($#v11_scmyciel :::"finitely_colorable"::: )    ($#m1_hidden :::"SimpleGraph":::); let "n" be   ($#m1_hidden :::"Nat":::); 
cluster (Set (Set  "("  ($#k13_scmyciel :::"MycielskianSeq"::: )  "G" ")" )  ($#k1_funct_1 :::"."::: )  "n") ->   ($#v11_scmyciel :::"finitely_colorable"::: )   ; 
end; registrationlet "G" be   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"SimpleGraph":::); let "n" be   ($#m1_hidden :::"Nat":::); 
cluster (Set (Set  "("  ($#k13_scmyciel :::"MycielskianSeq"::: )  "G" ")" )  ($#k1_funct_1 :::"."::: )  "n") ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; 
theorem :: SCMYCIEL:116 (Bool  "for" (Set (Var "G")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k2_scmyciel :::"order"::: )  (Set  "(" (Set  "("  ($#k13_scmyciel :::"MycielskianSeq"::: )  (Set (Var "G")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Num 2)  ($#k2_newton :::"|^"::: )  (Set (Var "n")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k2_scmyciel :::"order"::: )  (Set (Var "G")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Num 2)  ($#k2_newton :::"|^"::: )  (Set (Var "n")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Num 1))))) ; 
 
theorem :: SCMYCIEL:117 (Bool  "for" (Set (Var "G")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"SimpleGraph":::)  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k3_scmyciel :::"size"::: )  (Set  "(" (Set  "("  ($#k13_scmyciel :::"MycielskianSeq"::: )  (Set (Var "G")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Num 3)  ($#k2_newton :::"|^"::: )  (Set (Var "n")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k3_scmyciel :::"size"::: )  (Set (Var "G")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Num 3)  ($#k2_newton :::"|^"::: )  (Set (Var "n")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k2_newton :::"|^"::: )  (Set (Var "n")) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k2_scmyciel :::"order"::: )  (Set (Var "G")) ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" )  ($#k3_stirl2_1 :::"block"::: )  (Num 3) ")" ))))) ; 
 
theorem :: SCMYCIEL:118 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set   ($#k8_scmyciel :::"clique#"::: )  (Set  "(" (Set  "("  ($#k13_scmyciel :::"MycielskianSeq"::: )  (Set  "("  ($#k5_scmyciel :::"CompleteSGraph"::: )  (Num 2) ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Num 2)) & (Bool (Set   ($#k10_scmyciel :::"chromatic#"::: )  (Set  "(" (Set  "("  ($#k13_scmyciel :::"MycielskianSeq"::: )  (Set  "("  ($#k5_scmyciel :::"CompleteSGraph"::: )  (Num 2) ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2)))  ")" )) ; 
 
theorem :: SCMYCIEL:119 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) (Bool  "ex" (Set (Var "G")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"SimpleGraph":::) "st"  (Bool  "("  (Bool (Set   ($#k8_scmyciel :::"clique#"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Num 2)) & (Bool (Set   ($#k10_scmyciel :::"chromatic#"::: )  (Set (Var "G")))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "n")))  ")" ))) ; 
 
theorem :: SCMYCIEL:120 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) (Bool  "ex" (Set (Var "G")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"SimpleGraph":::) "st"  (Bool  "("  (Bool (Set   ($#k11_scmyciel :::"stability#"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Num 2)) & (Bool (Set   ($#k9_scmyciel :::"cliquecover#"::: )  (Set (Var "G")))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "n")))  ")" ))) ;