:: KURATO_1 semantic presentation begin notationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); synonym "A" :::"-"::: for :::"Cl"::: "A"; end; theorem :: KURATO_1:1 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "A")) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) )))) ; definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); func :::"Kurat14Part"::: "A" -> ($#m1_hidden :::"set"::: ) equals :: KURATO_1:def 1 (Set ($#k5_enumset1 :::"{"::: ) "A" "," (Set "(" "A" ($#k2_pre_topc :::"-"::: ) ")" ) "," (Set "(" (Set "(" "A" ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" "A" ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" "A" ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" "A" ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" "A" ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k5_enumset1 :::"}"::: ) ); end; :: deftheorem defines :::"Kurat14Part"::: KURATO_1:def 1 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k1_kurato_1 :::"Kurat14Part"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k5_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set "(" (Set (Var "A")) ($#k2_pre_topc :::"-"::: ) ")" ) "," (Set "(" (Set "(" (Set (Var "A")) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k5_enumset1 :::"}"::: ) )))); registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); cluster (Set ($#k1_kurato_1 :::"Kurat14Part"::: ) "A") -> ($#v1_finset_1 :::"finite"::: ) ; end; definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); func :::"Kurat14Set"::: "A" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "T" equals :: KURATO_1:def 2 (Set (Set ($#k5_enumset1 :::"{"::: ) "A" "," (Set "(" "A" ($#k2_pre_topc :::"-"::: ) ")" ) "," (Set "(" (Set "(" "A" ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" "A" ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" "A" ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" "A" ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" "A" ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k5_enumset1 :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k5_enumset1 :::"{"::: ) (Set "(" "A" ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set "(" (Set "(" "A" ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" "A" ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" "A" ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" "A" ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" "A" ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" "A" ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k5_enumset1 :::"}"::: ) )); end; :: deftheorem defines :::"Kurat14Set"::: KURATO_1:def 2 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k2_kurato_1 :::"Kurat14Set"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k5_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set "(" (Set (Var "A")) ($#k2_pre_topc :::"-"::: ) ")" ) "," (Set "(" (Set "(" (Set (Var "A")) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k5_enumset1 :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k5_enumset1 :::"{"::: ) (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set "(" (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k5_enumset1 :::"}"::: ) ))))); theorem :: KURATO_1:2 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k2_kurato_1 :::"Kurat14Set"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_kurato_1 :::"Kurat14Part"::: ) (Set (Var "A")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k1_kurato_1 :::"Kurat14Part"::: ) (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ))))) ; theorem :: KURATO_1:3 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k2_kurato_1 :::"Kurat14Set"::: ) (Set (Var "A")))) & (Bool (Set (Set (Var "A")) ($#k2_pre_topc :::"-"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_kurato_1 :::"Kurat14Set"::: ) (Set (Var "A")))) & (Bool (Set (Set "(" (Set (Var "A")) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_kurato_1 :::"Kurat14Set"::: ) (Set (Var "A")))) & (Bool (Set (Set "(" (Set "(" (Set (Var "A")) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_kurato_1 :::"Kurat14Set"::: ) (Set (Var "A")))) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_kurato_1 :::"Kurat14Set"::: ) (Set (Var "A")))) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_kurato_1 :::"Kurat14Set"::: ) (Set (Var "A")))) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_kurato_1 :::"Kurat14Set"::: ) (Set (Var "A")))) ")" ))) ; theorem :: KURATO_1:4 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_kurato_1 :::"Kurat14Set"::: ) (Set (Var "A")))) & (Bool (Set (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_kurato_1 :::"Kurat14Set"::: ) (Set (Var "A")))) & (Bool (Set (Set "(" (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_kurato_1 :::"Kurat14Set"::: ) (Set (Var "A")))) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_kurato_1 :::"Kurat14Set"::: ) (Set (Var "A")))) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_kurato_1 :::"Kurat14Set"::: ) (Set (Var "A")))) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_kurato_1 :::"Kurat14Set"::: ) (Set (Var "A")))) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_kurato_1 :::"Kurat14Set"::: ) (Set (Var "A")))) ")" ))) ; definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); func :::"Kurat14ClPart"::: "A" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "T" equals :: KURATO_1:def 3 (Set ($#k4_enumset1 :::"{"::: ) (Set "(" "A" ($#k2_pre_topc :::"-"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" "A" ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" "A" ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) "," (Set "(" (Set "(" "A" ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" "A" ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" "A" ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k4_enumset1 :::"}"::: ) ); func :::"Kurat14OpPart"::: "A" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "T" equals :: KURATO_1:def 4 (Set ($#k4_enumset1 :::"{"::: ) (Set "(" (Set "(" "A" ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" "A" ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" "A" ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" "A" ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" "A" ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" "A" ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k4_enumset1 :::"}"::: ) ); end; :: deftheorem defines :::"Kurat14ClPart"::: KURATO_1:def 3 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k3_kurato_1 :::"Kurat14ClPart"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k4_enumset1 :::"{"::: ) (Set "(" (Set (Var "A")) ($#k2_pre_topc :::"-"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) "," (Set "(" (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k4_enumset1 :::"}"::: ) )))); :: deftheorem defines :::"Kurat14OpPart"::: KURATO_1:def 4 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k4_kurato_1 :::"Kurat14OpPart"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k4_enumset1 :::"{"::: ) (Set "(" (Set "(" (Set (Var "A")) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_pre_topc :::"-"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k4_enumset1 :::"}"::: ) )))); theorem :: KURATO_1:5 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k2_kurato_1 :::"Kurat14Set"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k2_tarski :::"{"::: ) (Set (Var "A")) "," (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k3_kurato_1 :::"Kurat14ClPart"::: ) (Set (Var "A")) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_kurato_1 :::"Kurat14OpPart"::: ) (Set (Var "A")) ")" ))))) ; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); cluster (Set ($#k2_kurato_1 :::"Kurat14Set"::: ) "A") -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: KURATO_1:6 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "Q")) ($#r2_hidden :::"in"::: ) (Set ($#k2_kurato_1 :::"Kurat14Set"::: ) (Set (Var "A"))))) "holds" (Bool "(" (Bool (Set (Set (Var "Q")) ($#k3_subset_1 :::"`"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_kurato_1 :::"Kurat14Set"::: ) (Set (Var "A")))) & (Bool (Set (Set (Var "Q")) ($#k2_pre_topc :::"-"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_kurato_1 :::"Kurat14Set"::: ) (Set (Var "A")))) ")" ))) ; theorem :: KURATO_1:7 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_kurato_1 :::"Kurat14Set"::: ) (Set (Var "A")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Num 14)))) ; begin definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); func :::"Kurat7Set"::: "A" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "T" equals :: KURATO_1:def 5 (Set ($#k5_enumset1 :::"{"::: ) "A" "," (Set "(" ($#k1_tops_1 :::"Int"::: ) "A" ")" ) "," (Set "(" ($#k2_pre_topc :::"Cl"::: ) "A" ")" ) "," (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) "A" ")" ) ")" ) "," (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) "A" ")" ) ")" ) "," (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) "A" ")" ) ")" ) ")" ) "," (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) "A" ")" ) ")" ) ")" ) ($#k5_enumset1 :::"}"::: ) ); end; :: deftheorem defines :::"Kurat7Set"::: KURATO_1:def 5 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k5_kurato_1 :::"Kurat7Set"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k5_enumset1 :::"{"::: ) (Set (Var "A")) "," (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" ) ")" ) "," (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" ) ")" ) "," (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" ) ")" ) ")" ) "," (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" ) ")" ) ")" ) ($#k5_enumset1 :::"}"::: ) )))); theorem :: KURATO_1:8 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k5_kurato_1 :::"Kurat7Set"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k1_tarski :::"{"::: ) (Set (Var "A")) ($#k1_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" ) ")" ) "," (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" ) ")" ) ")" ) ($#k1_enumset1 :::"}"::: ) ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" ) ")" ) "," (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" ) ")" ) ")" ) ($#k1_enumset1 :::"}"::: ) ))))) ; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); cluster (Set ($#k5_kurato_1 :::"Kurat7Set"::: ) "A") -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: KURATO_1:9 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "Q")) ($#r2_hidden :::"in"::: ) (Set ($#k5_kurato_1 :::"Kurat7Set"::: ) (Set (Var "A"))))) "holds" (Bool "(" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "Q"))) ($#r2_hidden :::"in"::: ) (Set ($#k5_kurato_1 :::"Kurat7Set"::: ) (Set (Var "A")))) & (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "Q"))) ($#r2_hidden :::"in"::: ) (Set ($#k5_kurato_1 :::"Kurat7Set"::: ) (Set (Var "A")))) ")" ))) ; begin definitionfunc :::"KurExSet"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) equals :: KURATO_1:def 6 (Set (Set "(" (Set "(" (Set ($#k1_seq_4 :::"{"::: ) (Num 1) ($#k1_seq_4 :::"}"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_borsuk_5 :::"RAT"::: ) "(" (Num 2) "," (Num 4) ")" ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Num 4) "," (Num 5) ($#k2_rcomp_1 :::".["::: ) ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Num 5) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k2_rcomp_1 :::".["::: ) )); end; :: deftheorem defines :::"KurExSet"::: KURATO_1:def 6 : (Bool (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k1_seq_4 :::"{"::: ) (Num 1) ($#k1_seq_4 :::"}"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_borsuk_5 :::"RAT"::: ) "(" (Num 2) "," (Num 4) ")" ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Num 4) "," (Num 5) ($#k2_rcomp_1 :::".["::: ) ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Num 5) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k2_rcomp_1 :::".["::: ) ))); theorem :: KURATO_1:10 (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_seq_4 :::"{"::: ) (Num 1) ($#k1_seq_4 :::"}"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Num 2) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k3_rcomp_1 :::".["::: ) ))) ; theorem :: KURATO_1:11 (Bool (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Num 1) "," (Num 2) ($#k2_rcomp_1 :::".["::: ) ))) ; theorem :: KURATO_1:12 (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Num 2) ($#k4_rcomp_1 :::".]"::: ) )) ; theorem :: KURATO_1:13 (Bool (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Num 2) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k2_rcomp_1 :::".["::: ) )) ; theorem :: KURATO_1:14 (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Num 2) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k3_rcomp_1 :::".["::: ) )) ; theorem :: KURATO_1:15 (Bool (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Num 2) ($#k2_rcomp_1 :::".["::: ) )) ; theorem :: KURATO_1:16 (Bool (Set (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Num 1) "," (Num 2) ($#k4_rcomp_1 :::".]"::: ) ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_borsuk_5 :::"IRRAT"::: ) "(" (Num 2) "," (Num 4) ")" ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k1_seq_4 :::"{"::: ) (Num 4) ($#k1_seq_4 :::"}"::: ) ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k1_seq_4 :::"{"::: ) (Num 5) ($#k1_seq_4 :::"}"::: ) ))) ; theorem :: KURATO_1:17 (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ($#k3_subset_1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Num 4) ($#k4_rcomp_1 :::".]"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k1_seq_4 :::"{"::: ) (Num 5) ($#k1_seq_4 :::"}"::: ) ))) ; theorem :: KURATO_1:18 (Bool (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_rcomp_1 :::"]."::: ) (Num 4) "," (Num 5) ($#k2_rcomp_1 :::".["::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Num 5) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k2_rcomp_1 :::".["::: ) ))) ; theorem :: KURATO_1:19 (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Num 4) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k3_rcomp_1 :::".["::: ) )) ; theorem :: KURATO_1:20 (Bool (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Num 4) ($#k2_rcomp_1 :::".["::: ) )) ; theorem :: KURATO_1:21 (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Num 4) ($#k4_rcomp_1 :::".]"::: ) )) ; theorem :: KURATO_1:22 (Bool (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Num 4) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k2_rcomp_1 :::".["::: ) )) ; begin theorem :: KURATO_1:23 (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_rcomp_1 :::"]."::: ) (Num 4) "," (Num 5) ($#k2_rcomp_1 :::".["::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Num 5) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k2_rcomp_1 :::".["::: ) ))) ; theorem :: KURATO_1:24 (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Num 4) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k3_rcomp_1 :::".["::: ) )) ; theorem :: KURATO_1:25 (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Num 4) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k2_rcomp_1 :::".["::: ) )) ; theorem :: KURATO_1:26 (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Num 2) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k2_rcomp_1 :::".["::: ) )) ; theorem :: KURATO_1:27 (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Num 2) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k3_rcomp_1 :::".["::: ) )) ; begin theorem :: KURATO_1:28 (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ))) ; theorem :: KURATO_1:29 (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ))) ; theorem :: KURATO_1:30 (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ")" ))) ; theorem :: KURATO_1:31 (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ))) ; theorem :: KURATO_1:32 (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ))) ; theorem :: KURATO_1:33 (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ))) ; theorem :: KURATO_1:34 (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ")" ))) ; theorem :: KURATO_1:35 (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ))) ; theorem :: KURATO_1:36 (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ))) ; theorem :: KURATO_1:37 (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ))) ; theorem :: KURATO_1:38 (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ))) ; theorem :: KURATO_1:39 (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) )) ($#r1_hidden :::"<>"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ))) ; theorem :: KURATO_1:40 (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) )) ; theorem :: KURATO_1:41 (Bool (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ))) ; theorem :: KURATO_1:42 (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ")" ))) ; theorem :: KURATO_1:43 (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ))) ; theorem :: KURATO_1:44 (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ))) ; begin theorem :: KURATO_1:45 (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ))) ; theorem :: KURATO_1:46 (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) )) "," (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" )) "," (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ")" )) ($#r1_zfmisc_1 :::"are_mutually_different"::: ) ) ; theorem :: KURATO_1:47 (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) )) "," (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" )) "," (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ")" )) ($#r1_zfmisc_1 :::"are_mutually_different"::: ) ) ; theorem :: KURATO_1:48 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) "," (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ")" ) "," (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ")" ) ")" ) ($#k1_enumset1 :::"}"::: ) ))) "holds" (Bool (Set (Var "X")) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ))) ; theorem :: KURATO_1:49 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) "," (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ")" ) "," (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ")" ) ")" ) ($#k1_enumset1 :::"}"::: ) ))) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) ; theorem :: KURATO_1:50 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) "," (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ")" ) "," (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ")" ) ")" ) ($#k1_enumset1 :::"}"::: ) ))) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) ; theorem :: KURATO_1:51 (Bool (Set ($#k1_enumset1 :::"{"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) "," (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ")" ) "," (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ")" ) ")" ) ($#k1_enumset1 :::"}"::: ) ) ($#r1_subset_1 :::"misses"::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) "," (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ")" ) "," (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ")" ) ")" ) ($#k1_enumset1 :::"}"::: ) )) ; theorem :: KURATO_1:52 (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) )) "," (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" )) "," (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ")" )) "," (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) )) "," (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" )) "," (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ")" )) ($#r4_zfmisc_1 :::"are_mutually_different"::: ) ) ; registration cluster (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) -> ($#~v3_pre_topc "non" ($#v3_pre_topc :::"open"::: ) ) ($#~v4_pre_topc "non" ($#v4_pre_topc :::"closed"::: ) ) ; end; theorem :: KURATO_1:53 (Bool (Set ($#k4_enumset1 :::"{"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) "," (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ")" ) "," (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ")" ) ")" ) "," (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) "," (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ")" ) "," (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ")" ) ")" ) ($#k4_enumset1 :::"}"::: ) ) ($#r1_subset_1 :::"misses"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ($#k1_tarski :::"}"::: ) )) ; theorem :: KURATO_1:54 (Bool (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) "," (Set ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) )) "," (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" )) "," (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ")" )) "," (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) )) "," (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" )) "," (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" ) ")" )) ($#r5_zfmisc_1 :::"are_mutually_different"::: ) ) ; theorem :: KURATO_1:55 (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k5_kurato_1 :::"Kurat7Set"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 7)) ; begin registration cluster (Set ($#k3_kurato_1 :::"Kurat14ClPart"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) )) -> ($#v3_setfam_1 :::"with_proper_subsets"::: ) ; cluster (Set ($#k4_kurato_1 :::"Kurat14OpPart"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) )) -> ($#v3_setfam_1 :::"with_proper_subsets"::: ) ; end; registration cluster (Set ($#k2_kurato_1 :::"Kurat14Set"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) )) -> ($#v3_setfam_1 :::"with_proper_subsets"::: ) ; end; registration cluster (Set ($#k2_kurato_1 :::"Kurat14Set"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) )) -> ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ; end; theorem :: KURATO_1:56 (Bool "for" (Set (Var "A")) "being" ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "B")) "is" ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ))) ; registration cluster (Set ($#k3_kurato_1 :::"Kurat14ClPart"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) )) -> ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ; cluster (Set ($#k4_kurato_1 :::"Kurat14OpPart"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) )) -> ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ; end; registration cluster ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ($#v3_setfam_1 :::"with_proper_subsets"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k3_topmetr :::"R^1"::: ) )) ")" )); end; theorem :: KURATO_1:57 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ($#v3_setfam_1 :::"with_proper_subsets"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_tops_2 :::"open"::: ) ) & (Bool (Set (Var "G")) "is" ($#v2_tops_2 :::"closed"::: ) )) "holds" (Bool (Set (Var "F")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "G")))) ; registration cluster (Set ($#k3_kurato_1 :::"Kurat14ClPart"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) )) -> ($#v2_tops_2 :::"closed"::: ) ; cluster (Set ($#k4_kurato_1 :::"Kurat14OpPart"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) )) -> ($#v1_tops_2 :::"open"::: ) ; end; theorem :: KURATO_1:58 (Bool (Set ($#k3_kurato_1 :::"Kurat14ClPart"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) )) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k4_kurato_1 :::"Kurat14OpPart"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ))) ; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); cluster (Set ($#k3_kurato_1 :::"Kurat14ClPart"::: ) "A") -> ($#v1_finset_1 :::"finite"::: ) ; cluster (Set ($#k4_kurato_1 :::"Kurat14OpPart"::: ) "A") -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: KURATO_1:59 (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k3_kurato_1 :::"Kurat14ClPart"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 6)) ; theorem :: KURATO_1:60 (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k4_kurato_1 :::"Kurat14OpPart"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 6)) ; theorem :: KURATO_1:61 (Bool (Set ($#k2_tarski :::"{"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) "," (Set "(" (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_tarski :::"}"::: ) ) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k3_kurato_1 :::"Kurat14ClPart"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ))) ; registration cluster (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: KURATO_1:62 (Bool (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ($#k3_subset_1 :::"`"::: ) )) ; theorem :: KURATO_1:63 (Bool (Set ($#k2_tarski :::"{"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) "," (Set "(" (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k2_tarski :::"}"::: ) ) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k4_kurato_1 :::"Kurat14OpPart"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ))) ; theorem :: KURATO_1:64 (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_kurato_1 :::"Kurat14Set"::: ) (Set ($#k6_kurato_1 :::"KurExSet"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 14)) ; begin definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "A" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "T")); attr "A" is :::"Cl-closed"::: means :: KURATO_1:def 7 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) "A")) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "P"))) ($#r2_hidden :::"in"::: ) "A")); attr "A" is :::"Int-closed"::: means :: KURATO_1:def 8 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) "A")) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "P"))) ($#r2_hidden :::"in"::: ) "A")); end; :: deftheorem defines :::"Cl-closed"::: KURATO_1:def 7 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_kurato_1 :::"Cl-closed"::: ) ) "iff" (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "P"))) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) ")" ))); :: deftheorem defines :::"Int-closed"::: KURATO_1:def 8 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_kurato_1 :::"Int-closed"::: ) ) "iff" (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "P")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "P"))) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) ")" ))); registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); cluster (Set ($#k2_kurato_1 :::"Kurat14Set"::: ) "A") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set ($#k2_kurato_1 :::"Kurat14Set"::: ) "A") -> ($#v1_kurato_1 :::"Cl-closed"::: ) ; cluster (Set ($#k2_kurato_1 :::"Kurat14Set"::: ) "A") -> ($#v1_prob_1 :::"compl-closed"::: ) ; end; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); cluster (Set ($#k5_kurato_1 :::"Kurat7Set"::: ) "A") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set ($#k5_kurato_1 :::"Kurat7Set"::: ) "A") -> ($#v2_kurato_1 :::"Int-closed"::: ) ; cluster (Set ($#k5_kurato_1 :::"Kurat7Set"::: ) "A") -> ($#v1_kurato_1 :::"Cl-closed"::: ) ; end; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_kurato_1 :::"Cl-closed"::: ) ($#v2_kurato_1 :::"Int-closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ")" )); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_prob_1 :::"compl-closed"::: ) ($#v1_kurato_1 :::"Cl-closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ")" )); end;