:: CANTOR_1  semantic presentation begin  definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "A" be   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); func  :::"UniCl"::: "A" ->   ($#m1_subset_1 :::"Subset-Family":::) "of" "X" means :: CANTOR_1:def 1 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "X" "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "ex" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" "X" "st"  (Bool  "("  (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  "A") & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_setfam_1 :::"union"::: )  (Set (Var "Y"))))  ")" ))  ")" )); end; 






:: deftheorem    defines :::"UniCl"::: CANTOR_1:def 1 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_cantor_1 :::"UniCl"::: )  (Set (Var "A")))) "iff" (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b3"))) "iff" (Bool  "ex" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st"  (Bool  "("  (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set (Var "A"))) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_setfam_1 :::"union"::: )  (Set (Var "Y"))))  ")" ))  ")" ))  ")" ))); 
 definitionlet "X" be    ($#l1_pre_topc :::"TopStruct"::: )  ; let "F" be   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); attr "F" is  :::"quasi_basis":::  means :: CANTOR_1:def 2 (Bool (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" "X")  ($#r1_tarski :::"c="::: )  (Set   ($#k1_cantor_1 :::"UniCl"::: )  "F")); end; 





:: deftheorem    defines :::"quasi_basis"::: CANTOR_1:def 2 :  (Bool  "for" (Set (Var "X")) "being"    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v1_cantor_1 :::"quasi_basis"::: )  ) "iff" (Bool (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "X")))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_cantor_1 :::"UniCl"::: )  (Set (Var "F"))))  ")" ))); 
 registrationlet "X" be    ($#l1_pre_topc :::"TopStruct"::: )  ; 
cluster (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" "X") ->   ($#v1_cantor_1 :::"quasi_basis"::: )   ; 
end; registrationlet "X" be    ($#l1_pre_topc :::"TopStruct"::: )  ; 
cluster   ($#v1_tops_2 :::"open"::: )     ($#v1_cantor_1 :::"quasi_basis"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "X") ")" )); 
end; definitionlet "X" be    ($#l1_pre_topc :::"TopStruct"::: )  ; mode Basis of "X" is   ($#v1_tops_2 :::"open"::: )     ($#v1_cantor_1 :::"quasi_basis"::: )    ($#m1_subset_1 :::"Subset-Family":::) "of" "X"; end; 
theorem :: CANTOR_1:1 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_cantor_1 :::"UniCl"::: )  (Set (Var "A")))))) ; 
 
theorem :: CANTOR_1:2 (Bool  "for" (Set (Var "S")) "being"    ($#l1_pre_topc :::"TopStruct"::: )   "holds"  (Bool (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "S"))) "is"   ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "S")))) ; 
 
theorem :: CANTOR_1:3 (Bool  "for" (Set (Var "S")) "being"    ($#l1_pre_topc :::"TopStruct"::: )   "holds"  (Bool (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "S"))) "is"   ($#v1_tops_2 :::"open"::: )  )) ; 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "A" be   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); func  :::"FinMeetCl"::: "A" ->   ($#m1_subset_1 :::"Subset-Family":::) "of" "X" means :: CANTOR_1:def 3 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "X" "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "ex" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" "X" "st"  (Bool  "("  (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  "A") & (Bool (Set (Var "Y")) "is"   ($#v1_finset_1 :::"finite"::: )  ) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_setfam_1 :::"Intersect"::: )  (Set (Var "Y"))))  ")" ))  ")" )); end; 






:: deftheorem    defines :::"FinMeetCl"::: CANTOR_1:def 3 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_cantor_1 :::"FinMeetCl"::: )  (Set (Var "A")))) "iff" (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b3"))) "iff" (Bool  "ex" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st"  (Bool  "("  (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set (Var "A"))) & (Bool (Set (Var "Y")) "is"   ($#v1_finset_1 :::"finite"::: )  ) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_setfam_1 :::"Intersect"::: )  (Set (Var "Y"))))  ")" ))  ")" ))  ")" ))); 
 
theorem :: CANTOR_1:4 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_cantor_1 :::"FinMeetCl"::: )  (Set (Var "A")))))) ; 
 
theorem :: CANTOR_1:5 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_cantor_1 :::"FinMeetCl"::: )  (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T")))))) ; 
 
theorem :: CANTOR_1:6 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_cantor_1 :::"UniCl"::: )  (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T")))))) ; 
 
theorem :: CANTOR_1:7 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_cantor_1 :::"UniCl"::: )  (Set  "("  ($#k2_cantor_1 :::"FinMeetCl"::: )  (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T"))) ")" )))) ; 
 
theorem :: CANTOR_1:8 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_cantor_1 :::"FinMeetCl"::: )  (Set (Var "A")))))) ; 
 
theorem :: CANTOR_1:9 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "B")))) "holds"  (Bool (Set   ($#k1_cantor_1 :::"UniCl"::: )  (Set (Var "A")))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_cantor_1 :::"UniCl"::: )  (Set (Var "B")))))) ; 
 
theorem :: CANTOR_1:10 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "("  ($#k9_setfam_1 :::"bool"::: )  (Set (Var "X")) ")" )  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "F"))  ($#r1_hidden :::"="::: )   "{"  (Set  "("  ($#k8_setfam_1 :::"Intersect"::: )  (Set (Var "x")) ")" ) where x "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set (Var "R")) : (Bool verum)  "}"  )) "holds"  (Bool (Set   ($#k8_setfam_1 :::"Intersect"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set   ($#k8_setfam_1 :::"Intersect"::: )  (Set  "("  ($#k5_setfam_1 :::"union"::: )  (Set (Var "R")) ")" )))))) ; 
 
theorem :: CANTOR_1:11 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k2_cantor_1 :::"FinMeetCl"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_cantor_1 :::"FinMeetCl"::: )  (Set  "("  ($#k2_cantor_1 :::"FinMeetCl"::: )  (Set (Var "A")) ")" ))))) ; 
 
theorem :: CANTOR_1:12 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_cantor_1 :::"FinMeetCl"::: )  (Set (Var "A")))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_cantor_1 :::"FinMeetCl"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set (Var "a"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "b")))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_cantor_1 :::"FinMeetCl"::: )  (Set (Var "A"))))))) ; 
 
theorem :: CANTOR_1:13 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_cantor_1 :::"FinMeetCl"::: )  (Set (Var "A")))) & (Bool (Set (Var "b"))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_cantor_1 :::"FinMeetCl"::: )  (Set (Var "A"))))) "holds"  (Bool (Set   ($#k3_setfam_1 :::"INTERSECTION"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k2_cantor_1 :::"FinMeetCl"::: )  (Set (Var "A"))))))) ; 
 
theorem :: CANTOR_1:14 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "B")))) "holds"  (Bool (Set   ($#k2_cantor_1 :::"FinMeetCl"::: )  (Set (Var "A")))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_cantor_1 :::"FinMeetCl"::: )  (Set (Var "B")))))) ; 
 registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; let "A" be   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); 
cluster (Set   ($#k2_cantor_1 :::"FinMeetCl"::: )  "A") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: CANTOR_1:15 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set (Var "X")) "," (Set  "("  ($#k1_cantor_1 :::"UniCl"::: )  (Set  "("  ($#k2_cantor_1 :::"FinMeetCl"::: )  (Set (Var "A")) ")" ) ")" ) "#)" ) "is"   ($#v2_pre_topc :::"TopSpace-like"::: )  ))) ; 
 definitionlet "X" be    ($#l1_pre_topc :::"TopStruct"::: )  ; let "F" be   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); attr "F" is  :::"quasi_prebasis":::  means :: CANTOR_1:def 4 (Bool  "ex" (Set (Var "G")) "being"   ($#m1_subset_1 :::"Basis":::) "of" "X" "st" (Bool (Set (Var "G"))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_cantor_1 :::"FinMeetCl"::: )  "F"))); end; 





:: deftheorem    defines :::"quasi_prebasis"::: CANTOR_1:def 4 :  (Bool  "for" (Set (Var "X")) "being"    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v2_cantor_1 :::"quasi_prebasis"::: )  ) "iff" (Bool  "ex" (Set (Var "G")) "being"   ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "X")) "st" (Bool (Set (Var "G"))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_cantor_1 :::"FinMeetCl"::: )  (Set (Var "F")))))  ")" ))); 
 registrationlet "X" be    ($#l1_pre_topc :::"TopStruct"::: )  ; 
cluster (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" "X") ->   ($#v2_cantor_1 :::"quasi_prebasis"::: )   ; 

cluster   ($#v1_tops_2 :::"open"::: )     ($#v1_cantor_1 :::"quasi_basis"::: )    ->   ($#v2_cantor_1 :::"quasi_prebasis"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "X") ")" )); 

cluster   ($#v1_tops_2 :::"open"::: )     ($#v2_cantor_1 :::"quasi_prebasis"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "X") ")" )); 
end; definitionlet "X" be    ($#l1_pre_topc :::"TopStruct"::: )  ; mode prebasis of "X" is   ($#v1_tops_2 :::"open"::: )     ($#v2_cantor_1 :::"quasi_prebasis"::: )    ($#m1_subset_1 :::"Subset-Family":::) "of" "X"; end; 
theorem :: CANTOR_1:16 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Var "Y")) "is"   ($#m1_subset_1 :::"Basis":::) "of" (Set  ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set (Var "X")) "," (Set  "("  ($#k1_cantor_1 :::"UniCl"::: )  (Set (Var "Y")) ")" ) "#)" )))) ; 
 
theorem :: CANTOR_1:17 (Bool  "for" (Set (Var "T1")) "," (Set (Var "T2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_pre_topc :::"strict"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"prebasis":::) "of" (Set (Var "T1"))  "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T1")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T2")))) & (Bool (Set (Var "P")) "is"   ($#m1_subset_1 :::"prebasis":::) "of" (Set (Var "T2")))) "holds"  (Bool (Set (Var "T1"))  ($#r1_hidden :::"="::: )  (Set (Var "T2"))))) ; 
 
theorem :: CANTOR_1:18 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Var "Y")) "is"   ($#m1_subset_1 :::"prebasis":::) "of" (Set  ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set (Var "X")) "," (Set  "("  ($#k1_cantor_1 :::"UniCl"::: )  (Set  "("  ($#k2_cantor_1 :::"FinMeetCl"::: )  (Set (Var "Y")) ")" ) ")" ) "#)" )))) ; 
 definitionfunc  :::"the_Cantor_set":::  ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_pre_topc :::"strict"::: )    ($#l1_pre_topc :::"TopSpace":::) means :: CANTOR_1:def 5 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set   ($#k4_card_3 :::"product"::: )  (Set  "(" (Set  ($#k5_numbers :::"NAT"::: ) )  ($#k7_funcop_1 :::"-->"::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k2_tarski :::"}"::: ) ) ")" ))) & (Bool  "ex" (Set (Var "P")) "being"   ($#m1_subset_1 :::"prebasis":::) "of" it "st"  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_card_3 :::"product"::: )  (Set  "(" (Set  ($#k5_numbers :::"NAT"::: ) )  ($#k7_funcop_1 :::"-->"::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k2_tarski :::"}"::: ) ) ")" ) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) "iff" (Bool  "ex" (Set (Var "N")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "for" (Set (Var "F")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_card_3 :::"product"::: )  (Set  "(" (Set  ($#k5_numbers :::"NAT"::: ) )  ($#k7_funcop_1 :::"-->"::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k2_tarski :::"}"::: ) ) ")" )) "holds"   (Bool  "("  (Bool (Set (Var "F"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) "iff" (Bool (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "N")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))  ")" )))  ")" )))  ")" ); end; 




:: deftheorem    defines :::"the_Cantor_set"::: CANTOR_1:def 5 :  (Bool  "for" (Set (Var "b1")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_pre_topc :::"strict"::: )    ($#l1_pre_topc :::"TopSpace":::) "holds"   (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_cantor_1 :::"the_Cantor_set"::: )  )) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b1")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_card_3 :::"product"::: )  (Set  "(" (Set  ($#k5_numbers :::"NAT"::: ) )  ($#k7_funcop_1 :::"-->"::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k2_tarski :::"}"::: ) ) ")" ))) & (Bool  "ex" (Set (Var "P")) "being"   ($#m1_subset_1 :::"prebasis":::) "of" (Set (Var "b1")) "st"  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_card_3 :::"product"::: )  (Set  "(" (Set  ($#k5_numbers :::"NAT"::: ) )  ($#k7_funcop_1 :::"-->"::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k2_tarski :::"}"::: ) ) ")" ) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) "iff" (Bool  "ex" (Set (Var "N")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "for" (Set (Var "F")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_card_3 :::"product"::: )  (Set  "(" (Set  ($#k5_numbers :::"NAT"::: ) )  ($#k7_funcop_1 :::"-->"::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k2_tarski :::"}"::: ) ) ")" )) "holds"   (Bool  "("  (Bool (Set (Var "F"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) "iff" (Bool (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "N")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))  ")" )))  ")" )))  ")" )  ")" ));