:: YELLOW13  semantic presentation begin  
theorem :: YELLOW13:1 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v7_pre_topc :::"T_1"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds"  (Bool (Set (Var "A")) "is"   ($#v4_pre_topc :::"closed"::: )  ))) ; 
 registrationlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v7_pre_topc :::"T_1"::: )    ($#l1_pre_topc :::"TopSpace":::); 
cluster   ($#v1_finset_1 :::"finite"::: )    ->   ($#v4_pre_topc :::"closed"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T")); 
end; registrationlet "T" be   ($#v1_compts_1 :::"compact"::: )     ($#l1_pre_topc :::"TopStruct"::: )  ; 
cluster (Set   ($#k2_struct_0 :::"[#]"::: )  "T") ->   ($#v2_compts_1 :::"compact"::: )   ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v8_struct_0 :::"finite"::: )     ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v7_pre_topc :::"T_1"::: )    ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_tdlat_3 :::"discrete"::: )    for    ($#l1_pre_topc :::"TopStruct"::: )  ; 
end; registration
cluster   ($#v8_struct_0 :::"finite"::: )     ($#v2_pre_topc :::"TopSpace-like"::: )    ->   ($#v1_compts_1 :::"compact"::: )    for    ($#l1_pre_topc :::"TopStruct"::: )  ; 
end; 
theorem :: YELLOW13:2 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_tdlat_3 :::"discrete"::: )    ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set (Var "T")) "is"   ($#v10_pre_topc :::"normal"::: )  )) ; 
 
theorem :: YELLOW13:3 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_tdlat_3 :::"discrete"::: )    ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set (Var "T")) "is"   ($#v9_pre_topc :::"regular"::: )  )) ; 
 
theorem :: YELLOW13:4 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_tdlat_3 :::"discrete"::: )    ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set (Var "T")) "is"   ($#v8_pre_topc :::"T_2"::: )  )) ; 
 
theorem :: YELLOW13:5 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_tdlat_3 :::"discrete"::: )    ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set (Var "T")) "is"   ($#v7_pre_topc :::"T_1"::: )  )) ; 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v1_tdlat_3 :::"discrete"::: )    ->   ($#v7_pre_topc :::"T_1"::: )     ($#v8_pre_topc :::"T_2"::: )     ($#v9_pre_topc :::"regular"::: )     ($#v10_pre_topc :::"normal"::: )    for    ($#l1_pre_topc :::"TopStruct"::: )  ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v12_pre_topc :::"T_4"::: )    ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v9_pre_topc :::"regular"::: )    for    ($#l1_pre_topc :::"TopStruct"::: )  ; 
end; registration
cluster   ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v11_pre_topc :::"T_3"::: )    ->   ($#v8_pre_topc :::"T_2"::: )    for    ($#l1_pre_topc :::"TopStruct"::: )  ; 
end; 
theorem :: YELLOW13:6 (Bool  "for" (Set (Var "S")) "being"   ($#v3_orders_2 :::"reflexive"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#v3_orders_2 :::"reflexive"::: )     ($#v4_orders_2 :::"transitive"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds"  (Bool (Set   ($#k3_waybel_0 :::"downarrow"::: )  (Set  "(" (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "X")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_waybel_0 :::"downarrow"::: )  (Set  "(" (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set  "("  ($#k3_waybel_0 :::"downarrow"::: )  (Set (Var "X")) ")" ) ")" ))))))) ; 
 
theorem :: YELLOW13:7 (Bool  "for" (Set (Var "S")) "being"   ($#v3_orders_2 :::"reflexive"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#v3_orders_2 :::"reflexive"::: )     ($#v4_orders_2 :::"transitive"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v5_orders_3 :::"monotone"::: )  )) "holds"  (Bool (Set   ($#k3_waybel_0 :::"downarrow"::: )  (Set  "(" (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_waybel_0 :::"downarrow"::: )  (Set  "(" (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set  "("  ($#k3_waybel_0 :::"downarrow"::: )  (Set (Var "X")) ")" ) ")" ))))))) ; 
 
theorem :: YELLOW13:8 (Bool  "for" (Set (Var "N")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_orders_2 :::"Poset":::) "holds"  (Bool (Set   ($#k3_yellow_2 :::"IdsMap"::: )  (Set (Var "N"))) "is" bbbadV2_FUNCT_1())) ; 
 registrationlet "N" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_orders_2 :::"Poset":::); 
cluster (Set   ($#k3_yellow_2 :::"IdsMap"::: )  "N") -> bbbadV2_FUNCT_1() ; 
end; 
theorem :: YELLOW13:9 (Bool  "for" (Set (Var "N")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"LATTICE":::) "holds"  (Bool (Set   ($#k2_yellow_2 :::"SupMap"::: )  (Set (Var "N"))) "is" bbbadV2_FUNCT_1())) ; 
 registrationlet "N" be   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"LATTICE":::); 
cluster (Set   ($#k2_yellow_2 :::"SupMap"::: )  "N") -> bbbadV2_FUNCT_1() ; 
end; 
theorem :: YELLOW13:10 (Bool  "for" (Set (Var "N")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"LATTICE":::) "holds"  (Bool (Set (Var "N")) "," (Set   ($#k2_yellow_1 :::"InclPoset"::: )  (Set  "("  ($#k7_waybel_0 :::"Ids"::: )  (Set (Var "N")) ")" ))  ($#r5_waybel_1 :::"are_isomorphic"::: )  )) ; 
 
theorem :: YELLOW13:11 (Bool  "for" (Set (Var "N")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_lattice3 :::"complete"::: )    ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N"))  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N")) "holds"  (Bool (Set (Set (Var "x"))  ($#k4_waybel_1 :::""/\""::: )  )  ($#r3_waybel_0 :::"preserves_inf_of"::: )  (Set (Var "X")))))) ; 
 
theorem :: YELLOW13:12 (Bool  "for" (Set (Var "N")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_lattice3 :::"complete"::: )    ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) "holds"  (Bool (Set (Set (Var "x"))  ($#k4_waybel_1 :::""/\""::: )  ) "is"   ($#v19_waybel_0 :::"meet-preserving"::: )  ))) ; 
 registrationlet "N" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_lattice3 :::"complete"::: )    ($#l1_orders_2 :::"Poset":::); let "x" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "N")); 
cluster (Set "x"  ($#k4_waybel_1 :::""/\""::: )  ) ->   ($#v19_waybel_0 :::"meet-preserving"::: )   ; 
end; begin  
theorem :: YELLOW13:13 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_tdlat_3 :::"anti-discrete"::: )     ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds"  (Bool (Set  ($#k1_tarski :::"{"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) ($#k1_tarski :::"}"::: ) ) "is"   ($#m1_subset_1 :::"Basis":::) "of" ))) ; 
 
theorem :: YELLOW13:14 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_tdlat_3 :::"anti-discrete"::: )     ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "D")) "being"   ($#m1_subset_1 :::"Basis":::) "of"  "holds"  (Bool (Set (Var "D"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) ($#k1_tarski :::"}"::: ) ))))) ; 
 
theorem :: YELLOW13:15 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds"  (Bool  "{"  (Set (Var "A")) where A "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) : (Bool  "("  (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))  ")" )  "}"   "is"   ($#m1_subset_1 :::"Basis":::) "of" )))) ; 
 
theorem :: YELLOW13:16 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds"   (Bool  "("  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_pre_topc :::"Cl"::: )  (Set (Var "A")))) "iff" (Bool  "for" (Set (Var "K")) "being"   ($#m1_subset_1 :::"Basis":::) "of"   (Bool  "for" (Set (Var "Q")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "Q"))  ($#r2_hidden :::"in"::: )  (Set (Var "K")))) "holds"  (Bool (Set (Var "A"))  ($#r1_xboole_0 :::"meets"::: )  (Set (Var "Q")))))  ")" )))) ; 
 
theorem :: YELLOW13:17 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds"   (Bool  "("  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_pre_topc :::"Cl"::: )  (Set (Var "A")))) "iff" (Bool  "ex" (Set (Var "K")) "being"   ($#m1_subset_1 :::"Basis":::) "of"  "st"  (Bool  "for" (Set (Var "Q")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "Q"))  ($#r2_hidden :::"in"::: )  (Set (Var "K")))) "holds"  (Bool (Set (Var "A"))  ($#r1_xboole_0 :::"meets"::: )  (Set (Var "Q")))))  ")" )))) ; 
 definitionlet "T" be    ($#l1_pre_topc :::"TopStruct"::: )  ; let "p" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); mode  :::"basis":::  "of" "p" ->   ($#m1_subset_1 :::"Subset-Family":::) "of" "T" means :: YELLOW13:def 1 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "T"  "st" (Bool (Bool "p"  ($#r2_hidden :::"in"::: )  (Set   ($#k1_tops_1 :::"Int"::: )  (Set (Var "A"))))) "holds"  (Bool  "ex" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "T" "st"  (Bool  "("  (Bool (Set (Var "P"))  ($#r2_hidden :::"in"::: )  it) & (Bool "p"  ($#r2_hidden :::"in"::: )  (Set   ($#k1_tops_1 :::"Int"::: )  (Set (Var "P")))) & (Bool (Set (Var "P"))  ($#r1_tarski :::"c="::: )  (Set (Var "A")))  ")" ))); end; 






:: deftheorem    defines :::"basis"::: YELLOW13:def 1 :  (Bool  "for" (Set (Var "T")) "being"    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds"   (Bool  "("  (Bool (Set (Var "b3")) "is"    ($#m1_yellow13 :::"basis"::: )   "of" (Set (Var "p"))) "iff" (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_tops_1 :::"Int"::: )  (Set (Var "A"))))) "holds"  (Bool  "ex" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st"  (Bool  "("  (Bool (Set (Var "P"))  ($#r2_hidden :::"in"::: )  (Set (Var "b3"))) & (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_tops_1 :::"Int"::: )  (Set (Var "P")))) & (Bool (Set (Var "P"))  ($#r1_tarski :::"c="::: )  (Set (Var "A")))  ")" )))  ")" )))); 
 definitionlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); let "p" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); redefine mode  :::"basis":::  "of" "p" means :: YELLOW13:def 2 (Bool  "for" (Set (Var "A")) "being"    ($#m1_connsp_2 :::"a_neighborhood"::: )   "of" "p" (Bool  "ex" (Set (Var "P")) "being"    ($#m1_connsp_2 :::"a_neighborhood"::: )   "of" "p" "st"  (Bool  "("  (Bool (Set (Var "P"))  ($#r2_hidden :::"in"::: )  it) & (Bool (Set (Var "P"))  ($#r1_tarski :::"c="::: )  (Set (Var "A")))  ")" ))); end; 






:: deftheorem    defines :::"basis"::: YELLOW13:def 2 :  (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds"   (Bool  "("  (Bool (Set (Var "b3")) "is"    ($#m1_yellow13 :::"basis"::: )   "of" (Set (Var "p"))) "iff" (Bool  "for" (Set (Var "A")) "being"    ($#m1_connsp_2 :::"a_neighborhood"::: )   "of" (Set (Var "p")) (Bool  "ex" (Set (Var "P")) "being"    ($#m1_connsp_2 :::"a_neighborhood"::: )   "of" (Set (Var "p")) "st"  (Bool  "("  (Bool (Set (Var "P"))  ($#r2_hidden :::"in"::: )  (Set (Var "b3"))) & (Bool (Set (Var "P"))  ($#r1_tarski :::"c="::: )  (Set (Var "A")))  ")" )))  ")" )))); 
 
theorem :: YELLOW13:18 (Bool  "for" (Set (Var "T")) "being"    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds"  (Bool (Set   ($#k9_setfam_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T")))) "is"    ($#m1_yellow13 :::"basis"::: )   "of" (Set (Var "p"))))) ; 
 
theorem :: YELLOW13:19 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "P")) "being"    ($#m1_yellow13 :::"basis"::: )   "of" (Set (Var "p"))  "holds" (Bool (Bool  "not" (Set (Var "P")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))))) ; 
 registrationlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); let "p" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); 
cluster   ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   for    ($#m1_yellow13 :::"basis"::: )   "of" "p"; 
end; registrationlet "T" be    ($#l1_pre_topc :::"TopStruct"::: )  ; let "p" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   for    ($#m1_yellow13 :::"basis"::: )   "of" "p"; 
end; definitionlet "T" be    ($#l1_pre_topc :::"TopStruct"::: )  ; let "p" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); let "P" be    ($#m1_yellow13 :::"basis"::: )   "of" (Set (Const "p")); attr "P" is  :::"correct":::  means :: YELLOW13:def 3 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "T" "holds"   (Bool  "("  (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  "P") "iff" (Bool "p"  ($#r2_hidden :::"in"::: )  (Set   ($#k1_tops_1 :::"Int"::: )  (Set (Var "A"))))  ")" )); end; 






:: deftheorem    defines :::"correct"::: YELLOW13:def 3 :  (Bool  "for" (Set (Var "T")) "being"    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "P")) "being"    ($#m1_yellow13 :::"basis"::: )   "of" (Set (Var "p")) "holds"   (Bool  "("  (Bool (Set (Var "P")) "is"   ($#v1_yellow13 :::"correct"::: )  ) "iff" (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds"   (Bool  "("  (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) "iff" (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_tops_1 :::"Int"::: )  (Set (Var "A"))))  ")" ))  ")" )))); 
 registrationlet "T" be    ($#l1_pre_topc :::"TopStruct"::: )  ; let "p" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); 
cluster   ($#v1_yellow13 :::"correct"::: )    for    ($#m1_yellow13 :::"basis"::: )   "of" "p"; 
end; 
theorem :: YELLOW13:20 (Bool  "for" (Set (Var "T")) "being"    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds"  (Bool  "{"  (Set (Var "A")) where A "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) : (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_tops_1 :::"Int"::: )  (Set (Var "A"))))  "}"   "is"   ($#v1_yellow13 :::"correct"::: )     ($#m1_yellow13 :::"basis"::: )   "of" (Set (Var "p"))))) ; 
 registrationlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); let "p" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_yellow13 :::"correct"::: )    for    ($#m1_yellow13 :::"basis"::: )   "of" "p"; 
end; 
theorem :: YELLOW13:21 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_tdlat_3 :::"anti-discrete"::: )     ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds"  (Bool (Set  ($#k1_tarski :::"{"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) ($#k1_tarski :::"}"::: ) ) "is"   ($#v1_yellow13 :::"correct"::: )     ($#m1_yellow13 :::"basis"::: )   "of" (Set (Var "p"))))) ; 
 
theorem :: YELLOW13:22 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_tdlat_3 :::"anti-discrete"::: )     ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "D")) "being"   ($#v1_yellow13 :::"correct"::: )     ($#m1_yellow13 :::"basis"::: )   "of" (Set (Var "p")) "holds"  (Bool (Set (Var "D"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) ($#k1_tarski :::"}"::: ) ))))) ; 
 
theorem :: YELLOW13:23 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Basis":::) "of"  "holds"  (Bool (Set (Var "P")) "is"    ($#m1_yellow13 :::"basis"::: )   "of" (Set (Var "p")))))) ; 
 definitionlet "T" be    ($#l1_pre_topc :::"TopStruct"::: )  ; mode  :::"basis":::  "of" "T" ->   ($#m1_subset_1 :::"Subset-Family":::) "of" "T" means :: YELLOW13:def 4 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" "T" "holds"  (Bool it "is"    ($#m1_yellow13 :::"basis"::: )   "of" (Set (Var "p")))); end; 





:: deftheorem    defines :::"basis"::: YELLOW13:def 4 :  (Bool  "for" (Set (Var "T")) "being"    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds"   (Bool  "("  (Bool (Set (Var "b2")) "is"    ($#m2_yellow13 :::"basis"::: )   "of" (Set (Var "T"))) "iff" (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds"  (Bool (Set (Var "b2")) "is"    ($#m1_yellow13 :::"basis"::: )   "of" (Set (Var "p"))))  ")" ))); 
 
theorem :: YELLOW13:24 (Bool  "for" (Set (Var "T")) "being"    ($#l1_pre_topc :::"TopStruct"::: )   "holds"  (Bool (Set   ($#k9_setfam_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T")))) "is"    ($#m2_yellow13 :::"basis"::: )   "of" (Set (Var "T")))) ; 
 
theorem :: YELLOW13:25 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "P")) "being"    ($#m2_yellow13 :::"basis"::: )   "of" (Set (Var "T"))  "holds" (Bool (Bool  "not" (Set (Var "P")) "is"   ($#v1_xboole_0 :::"empty"::: )  )))) ; 
 registrationlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); 
cluster   ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   for    ($#m2_yellow13 :::"basis"::: )   "of" "T"; 
end; registrationlet "T" be    ($#l1_pre_topc :::"TopStruct"::: )  ; 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   for    ($#m2_yellow13 :::"basis"::: )   "of" "T"; 
end; 
theorem :: YELLOW13:26 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "P")) "being"    ($#m2_yellow13 :::"basis"::: )   "of" (Set (Var "T")) "holds"  (Bool (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T")))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_cantor_1 :::"UniCl"::: )  (Set  "("  ($#k1_tdlat_2 :::"Int"::: )  (Set (Var "P")) ")" ))))) ; 
 
theorem :: YELLOW13:27 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")) "holds"  (Bool (Set (Var "P")) "is"    ($#m2_yellow13 :::"basis"::: )   "of" (Set (Var "T"))))) ; 
 definitionlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_pre_topc :::"TopSpace-like"::: )     ($#l1_waybel_9 :::"TopRelStr"::: )  ; attr "T" is  :::"topological_semilattice":::  means :: YELLOW13:def 5 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) "T" "," "T" ($#k2_borsuk_1 :::":]"::: ) ) "," "T"  "st" (Bool (Bool (Set (Var "f"))  ($#r1_funct_2 :::"="::: )  (Set   ($#k4_waybel_2 :::"inf_op"::: )  "T"))) "holds"  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  )); end; 




:: deftheorem    defines :::"topological_semilattice"::: YELLOW13:def 5 :  (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_pre_topc :::"TopSpace-like"::: )     ($#l1_waybel_9 :::"TopRelStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "T")) "is"   ($#v2_yellow13 :::"topological_semilattice"::: )  ) "iff" (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "T")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Var "T"))  "st" (Bool (Bool (Set (Var "f"))  ($#r1_funct_2 :::"="::: )  (Set   ($#k4_waybel_2 :::"inf_op"::: )  (Set (Var "T"))))) "holds"  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ))  ")" )); 
 registration
cluster (Num 1)  ($#v13_struct_0 :::"-element"::: )     ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v3_orders_2 :::"reflexive"::: )    -> (Num 1)  ($#v13_struct_0 :::"-element"::: )     ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v2_yellow13 :::"topological_semilattice"::: )    for    ($#l1_waybel_9 :::"TopRelStr"::: )  ; 
end; 
theorem :: YELLOW13:28 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v2_yellow13 :::"topological_semilattice"::: )     ($#l1_waybel_9 :::"TopRelStr"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "holds"  (Bool (Set (Set (Var "x"))  ($#k4_waybel_1 :::""/\""::: )  ) "is"   ($#v5_pre_topc :::"continuous"::: )  ))) ; 
 registrationlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v2_yellow13 :::"topological_semilattice"::: )     ($#l1_waybel_9 :::"TopRelStr"::: )  ; let "x" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "T")); 
cluster (Set "x"  ($#k4_waybel_1 :::""/\""::: )  ) ->   ($#v5_pre_topc :::"continuous"::: )   ; 
end;