:: YELLOW14  semantic presentation begin  
theorem :: YELLOW14:1 (Bool (Set   ($#k9_setfam_1 :::"bool"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k2_tarski :::"}"::: ) )) ; 
 
theorem :: YELLOW14:2 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set  "(" (Set  "("  ($#k6_partfun1 :::"id"::: )  (Set (Var "X")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set (Var "Y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "Y"))))) ; 
 
theorem :: YELLOW14:3 (Bool  "for" (Set (Var "S")) "being"   ($#v2_struct_0 :::"empty"::: )     ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "T")) "being"    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))  "st" (Bool (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T"))))) "holds"  (Bool (Set (Var "T")) "is"   ($#v2_struct_0 :::"empty"::: )  )))) ; 
 
theorem :: YELLOW14:4 (Bool  "for" (Set (Var "S")) "being"    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#v2_struct_0 :::"empty"::: )     ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))  "st" (Bool (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "S"))))) "holds"  (Bool (Set (Var "S")) "is"   ($#v2_struct_0 :::"empty"::: )  )))) ; 
 
theorem :: YELLOW14:5 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "T")) "being"    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))  "st" (Bool (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "S"))))) "holds"  (Bool  "not" (Bool (Set (Var "T")) "is"   ($#v2_struct_0 :::"empty"::: )  ))))) ; 
 
theorem :: YELLOW14:6 (Bool  "for" (Set (Var "S")) "being"    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))  "st" (Bool (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T"))))) "holds"  (Bool  "not" (Bool (Set (Var "S")) "is"   ($#v2_struct_0 :::"empty"::: )  ))))) ; 
 definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; let "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set (Const "T")); redefine attr "f" is  :::"directed-sups-preserving":::  means :: YELLOW14:def 1 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_waybel_0 :::"directed"::: )    ($#m1_subset_1 :::"Subset":::) "of" "S" "holds"  (Bool "f"  ($#r4_waybel_0 :::"preserves_sup_of"::: )  (Set (Var "X")))); end; 






:: deftheorem    defines :::"directed-sups-preserving"::: YELLOW14:def 1 :  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v22_waybel_0 :::"directed-sups-preserving"::: )  ) "iff" (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_waybel_0 :::"directed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds"  (Bool (Set (Var "f"))  ($#r4_waybel_0 :::"preserves_sup_of"::: )  (Set (Var "X"))))  ")" )))); 
 definitionlet "R" be    ($#l1_struct_0 :::"1-sorted"::: )  ; let "N" be    ($#l1_waybel_0 :::"NetStr"::: )   "over" (Set (Const "R")); attr "N" is  :::"Function-yielding":::  means :: YELLOW14:def 2 (Bool (Set  "the"  ($#u1_waybel_0 :::"mapping"::: )  "of" "N") "is"   ($#v1_funcop_1 :::"Function-yielding"::: )  ); end; 





:: deftheorem    defines :::"Function-yielding"::: YELLOW14:def 2 :  (Bool  "for" (Set (Var "R")) "being"    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "N")) "being"    ($#l1_waybel_0 :::"NetStr"::: )   "over" (Set (Var "R")) "holds"   (Bool  "("  (Bool (Set (Var "N")) "is"   ($#v1_yellow14 :::"Function-yielding"::: )  ) "iff" (Bool (Set  "the"  ($#u1_waybel_0 :::"mapping"::: )  "of" (Set (Var "N"))) "is"   ($#v1_funcop_1 :::"Function-yielding"::: )  )  ")" ))); 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_monoid_0 :::"constituted-Functions"::: )    for    ($#l1_struct_0 :::"1-sorted"::: )  ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_orders_2 :::"strict"::: )     ($#v1_monoid_0 :::"constituted-Functions"::: )    for    ($#l1_orders_2 :::"RelStr"::: )  ; 
end; registrationlet "R" be   ($#v1_monoid_0 :::"constituted-Functions"::: )     ($#l1_struct_0 :::"1-sorted"::: )  ; 
cluster   ->   ($#v1_yellow14 :::"Function-yielding"::: )    for    ($#l1_waybel_0 :::"NetStr"::: )   "over" "R"; 
end; registrationlet "R" be   ($#v1_monoid_0 :::"constituted-Functions"::: )     ($#l1_struct_0 :::"1-sorted"::: )  ; 
cluster   ($#v6_waybel_0 :::"strict"::: )     ($#v1_yellow14 :::"Function-yielding"::: )    for    ($#l1_waybel_0 :::"NetStr"::: )   "over" "R"; 
end; registrationlet "R" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_monoid_0 :::"constituted-Functions"::: )     ($#l1_struct_0 :::"1-sorted"::: )  ; 
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_waybel_0 :::"strict"::: )     ($#v1_yellow14 :::"Function-yielding"::: )    for    ($#l1_waybel_0 :::"NetStr"::: )   "over" "R"; 
end; registrationlet "R" be   ($#v1_monoid_0 :::"constituted-Functions"::: )     ($#l1_struct_0 :::"1-sorted"::: )  ; let "N" be   ($#v1_yellow14 :::"Function-yielding"::: )     ($#l1_waybel_0 :::"NetStr"::: )   "over" (Set (Const "R")); 
cluster (Set  "the"  ($#u1_waybel_0 :::"mapping"::: )  "of" "N") ->   ($#v1_funcop_1 :::"Function-yielding"::: )   ; 
end; registrationlet "R" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_monoid_0 :::"constituted-Functions"::: )     ($#l1_struct_0 :::"1-sorted"::: )  ; 
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v4_orders_2 :::"transitive"::: )     ($#v6_waybel_0 :::"strict"::: )     ($#v7_waybel_0 :::"directed"::: )     ($#v1_yellow14 :::"Function-yielding"::: )    for    ($#l1_waybel_0 :::"NetStr"::: )   "over" "R"; 
end; registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_struct_0 :::"1-sorted"::: )  ; let "N" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_waybel_0 :::"NetStr"::: )   "over" (Set (Const "S")); 
cluster (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "the"  ($#u1_waybel_0 :::"mapping"::: )  "of" "N")) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_struct_0 :::"1-sorted"::: )  ; let "N" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_waybel_0 :::"NetStr"::: )   "over" (Set (Const "S")); 
cluster (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k1_waybel_0 :::"netmap"::: )   "(" "N" "," "S" ")"  ")" )) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: YELLOW14:7 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "B")) "," (Set (Var "C"))  (Bool  "for" (Set (Var "g")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B"))  "st" (Bool (Bool (Set (Var "g"))  ($#r1_yellow_2 :::"<="::: )  (Set (Var "h"))) & (Bool (Set (Var "f")) "is"   ($#v5_orders_3 :::"monotone"::: )  )) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "g")))  ($#r1_yellow_2 :::"<="::: )  (Set (Set (Var "f"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "h"))))))) ; 
 
theorem :: YELLOW14:8 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_pre_topc :::"TopSpace-like"::: )     ($#l1_waybel_9 :::"TopRelStr"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k3_waybel24 :::"ContMaps"::: )   "(" (Set (Var "S")) "," (Set (Var "T")) ")"  ")" )  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "f"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "g")))) "holds"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "y"))) "iff" (Bool (Set (Var "f"))  ($#r1_yellow_2 :::"<="::: )  (Set (Var "g")))  ")" ))))) ; 
 definitionlet "I" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "R" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; let "f" be   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Const "R"))  ($#k6_yellow_1 :::"|^"::: )  (Set (Const "I")) ")" ); let "i" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "I")); :: original: :::"."::: redefine func "f" :::"."::: "i" ->   ($#m1_subset_1 :::"Element":::) "of" "R"; end; begin  
theorem :: YELLOW14:9 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v23_waybel_0 :::"isomorphic"::: )  )) "holds"  (Bool (Set (Var "f")) "is"   ($#v2_funct_2 :::"onto"::: )  ))) ; 
 registrationlet "S", "T" be    ($#l1_orders_2 :::"RelStr"::: )  ; 
cluster   ($#v1_funct_1 :::"Function-like"::: )     ($#v1_funct_2 :::"quasi_total"::: )     ($#v23_waybel_0 :::"isomorphic"::: )    ->   ($#v2_funct_2 :::"onto"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T"))))); 
end; 
theorem :: YELLOW14:10 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v23_waybel_0 :::"isomorphic"::: )  )) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_tops_2 :::"/""::: )  ) "is"   ($#v23_waybel_0 :::"isomorphic"::: )  ))) ; 
 
theorem :: YELLOW14:11 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    "st" (Bool (Bool (Set (Var "S")) "," (Set (Var "T"))  ($#r5_waybel_1 :::"are_isomorphic"::: )  ) & (Bool (Set (Var "S")) "is"   ($#v2_lattice3 :::"with_infima"::: )  )) "holds"  (Bool (Set (Var "T")) "is"   ($#v2_lattice3 :::"with_infima"::: )  )) ; 
 
theorem :: YELLOW14:12 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    "st" (Bool (Bool (Set (Var "S")) "," (Set (Var "T"))  ($#r5_waybel_1 :::"are_isomorphic"::: )  ) & (Bool (Set (Var "S")) "is"   ($#v1_lattice3 :::"with_suprema"::: )  )) "holds"  (Bool (Set (Var "T")) "is"   ($#v1_lattice3 :::"with_suprema"::: )  )) ; 
 
theorem :: YELLOW14:13 (Bool  "for" (Set (Var "L")) "being"    ($#l1_orders_2 :::"RelStr"::: )    "st" (Bool (Bool (Set (Var "L")) "is"   ($#v2_struct_0 :::"empty"::: )  )) "holds"  (Bool (Set (Var "L")) "is"   ($#v3_yellow_0 :::"bounded"::: )  )) ; 
 registration
cluster   ($#v2_struct_0 :::"empty"::: )    ->   ($#v3_yellow_0 :::"bounded"::: )    for    ($#l1_orders_2 :::"RelStr"::: )  ; 
end; 
theorem :: YELLOW14:14 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"    ($#l1_orders_2 :::"RelStr"::: )    "st" (Bool (Bool (Set (Var "S")) "," (Set (Var "T"))  ($#r5_waybel_1 :::"are_isomorphic"::: )  ) & (Bool (Set (Var "S")) "is"   ($#v1_yellow_0 :::"lower-bounded"::: )  )) "holds"  (Bool (Set (Var "T")) "is"   ($#v1_yellow_0 :::"lower-bounded"::: )  )) ; 
 
theorem :: YELLOW14:15 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"    ($#l1_orders_2 :::"RelStr"::: )    "st" (Bool (Bool (Set (Var "S")) "," (Set (Var "T"))  ($#r5_waybel_1 :::"are_isomorphic"::: )  ) & (Bool (Set (Var "S")) "is"   ($#v2_yellow_0 :::"upper-bounded"::: )  )) "holds"  (Bool (Set (Var "T")) "is"   ($#v2_yellow_0 :::"upper-bounded"::: )  )) ; 
 
theorem :: YELLOW14:16 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v23_waybel_0 :::"isomorphic"::: )  ) & (Bool   ($#r1_yellow_0 :::"ex_sup_of"::: )  (Set (Var "A")) "," (Set (Var "S")))) "holds"  (Bool   ($#r1_yellow_0 :::"ex_sup_of"::: )  (Set (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "A"))) "," (Set (Var "T")))))) ; 
 
theorem :: YELLOW14:17 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v23_waybel_0 :::"isomorphic"::: )  ) & (Bool   ($#r2_yellow_0 :::"ex_inf_of"::: )  (Set (Var "A")) "," (Set (Var "S")))) "holds"  (Bool   ($#r2_yellow_0 :::"ex_inf_of"::: )  (Set (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "A"))) "," (Set (Var "T")))))) ; 
 begin  
theorem :: YELLOW14:18 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"    ($#l1_pre_topc :::"TopStruct"::: )    "st" (Bool (Bool  "("  (Bool (Set (Var "S")) "," (Set (Var "T"))  ($#r1_t_0topsp :::"are_homeomorphic"::: )  ) "or" (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st"  (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "S")))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T"))))  ")" ))  ")" )) "holds"  (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v2_struct_0 :::"empty"::: )  ) "iff" (Bool (Set (Var "T")) "is"   ($#v2_struct_0 :::"empty"::: )  )  ")" )) ; 
 
theorem :: YELLOW14:19 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set (Var "T")) "," (Set   ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) "," (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T"))) "#)" )  ($#r1_t_0topsp :::"are_homeomorphic"::: )  )) ; 
 registrationlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v4_waybel11 :::"Scott"::: )     ($#l1_waybel_9 :::"TopRelStr"::: )  ; 
cluster   ($#v3_pre_topc :::"open"::: )    ->   ($#v13_waybel_0 :::"upper"::: )     ($#v1_waybel11 :::"inaccessible"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T"))); 

cluster   ($#v13_waybel_0 :::"upper"::: )     ($#v1_waybel11 :::"inaccessible"::: )    ->   ($#v3_pre_topc :::"open"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T"))); 
end; 
theorem :: YELLOW14:20 (Bool  "for" (Set (Var "T")) "being"    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set   ($#k2_pre_topc :::"Cl"::: )  (Set (Var "X")))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_pre_topc :::"Cl"::: )  (Set (Var "Y"))))) "holds"  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_pre_topc :::"Cl"::: )  (Set (Var "Y"))))))) ; 
 
theorem :: YELLOW14:21 (Bool  "for" (Set (Var "T")) "being"    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "Y")) "," (Set (Var "V")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "Y"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_pre_topc :::"Cl"::: )  (Set (Var "Y")))) & (Bool (Set (Var "V")) "is"   ($#v3_pre_topc :::"open"::: )  ) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "V")))) "holds"  (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "V")))))) ; 
 
theorem :: YELLOW14:22 (Bool  "for" (Set (Var "T")) "being"    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Var "Y"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) )) & (Bool  "("   "for" (Set (Var "V")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "V")) "is"   ($#v3_pre_topc :::"open"::: )  ) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "V")))) "holds"  (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "V")))  ")" )) "holds"  (Bool (Set   ($#k2_pre_topc :::"Cl"::: )  (Set (Var "X")))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_pre_topc :::"Cl"::: )  (Set (Var "Y"))))))) ; 
 
theorem :: YELLOW14:23 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#v3_yellow_8 :::"irreducible"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Var "B"))) & (Bool (Set   ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "," (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "S"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) "," (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T"))) "#)" ))) "holds"  (Bool (Set (Var "B")) "is"   ($#v3_yellow_8 :::"irreducible"::: )  )))) ; 
 
theorem :: YELLOW14:24 (Bool  "for" (Set (Var "S")) "," (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 :::"Point":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Var "B"))) & (Bool (Set   ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "," (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "S"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) "," (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T"))) "#)" )) & (Bool (Set (Var "a"))  ($#r1_yellow_8 :::"is_dense_point_of"::: )  (Set (Var "A")))) "holds"  (Bool (Set (Var "b"))  ($#r1_yellow_8 :::"is_dense_point_of"::: )  (Set (Var "B")))))))) ; 
 
theorem :: YELLOW14:25 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Var "B"))) & (Bool (Set   ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "," (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "S"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) "," (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T"))) "#)" )) & (Bool (Set (Var "A")) "is"   ($#v2_compts_1 :::"compact"::: )  )) "holds"  (Bool (Set (Var "B")) "is"   ($#v2_compts_1 :::"compact"::: )  )))) ; 
 
theorem :: YELLOW14:26 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Set   ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "," (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "S"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) "," (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T"))) "#)" )) & (Bool (Set (Var "S")) "is"   ($#v4_yellow_8 :::"sober"::: )  )) "holds"  (Bool (Set (Var "T")) "is"   ($#v4_yellow_8 :::"sober"::: )  )) ; 
 
theorem :: YELLOW14:27 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Set   ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "," (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "S"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) "," (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T"))) "#)" )) & (Bool (Set (Var "S")) "is"   ($#v6_waybel_3 :::"locally-compact"::: )  )) "holds"  (Bool (Set (Var "T")) "is"   ($#v6_waybel_3 :::"locally-compact"::: )  )) ; 
 
theorem :: YELLOW14:28 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"    ($#l1_pre_topc :::"TopStruct"::: )    "st" (Bool (Bool (Set   ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "," (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "S"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) "," (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T"))) "#)" )) & (Bool (Set (Var "S")) "is"   ($#v1_compts_1 :::"compact"::: )  )) "holds"  (Bool (Set (Var "T")) "is"   ($#v1_compts_1 :::"compact"::: )  )) ; 
 definitionlet "I" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); let "x" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k3_waybel18 :::"product"::: )  (Set  "(" (Set (Const "I"))  ($#k7_funcop_1 :::"-->"::: )  (Set (Const "T")) ")" ) ")" ); let "i" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "I")); :: original: :::"."::: redefine func "x" :::"."::: "i" ->   ($#m1_subset_1 :::"Element":::) "of" "T"; end; 
theorem :: YELLOW14:29 (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "being"   ($#v4_waybel_3 :::"non-Empty"::: )     ($#v1_waybel18 :::"TopStruct-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "M"))  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k3_waybel18 :::"product"::: )  (Set (Var "J")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_pre_topc :::"Cl"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) ))) "iff" (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "M")) "holds"  (Bool (Set (Set (Var "x"))  ($#k5_waybel18 :::"."::: )  (Set (Var "i")))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_pre_topc :::"Cl"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "(" (Set (Var "y"))  ($#k5_waybel18 :::"."::: )  (Set (Var "i")) ")" ) ($#k6_domain_1 :::"}"::: ) ))))  ")" )))) ; 
 
theorem :: YELLOW14:30 (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k3_waybel18 :::"product"::: )  (Set  "(" (Set (Var "M"))  ($#k7_funcop_1 :::"-->"::: )  (Set (Var "T")) ")" ) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_pre_topc :::"Cl"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) ))) "iff" (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "M")) "holds"  (Bool (Set (Set (Var "x"))  ($#k2_yellow14 :::"."::: )  (Set (Var "i")))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_pre_topc :::"Cl"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "(" (Set (Var "y"))  ($#k2_yellow14 :::"."::: )  (Set (Var "i")) ")" ) ($#k6_domain_1 :::"}"::: ) ))))  ")" )))) ; 
 
theorem :: YELLOW14:31 (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "M"))  (Bool  "for" (Set (Var "J")) "being"   ($#v4_waybel_3 :::"non-Empty"::: )     ($#v1_waybel18 :::"TopStruct-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "M"))  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k3_waybel18 :::"product"::: )  (Set (Var "J")) ")" ) "holds"  (Bool (Set   ($#k5_card_3 :::"pi"::: )   "(" (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ")" ) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k2_pre_topc :::"Cl"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "(" (Set (Var "x"))  ($#k5_waybel18 :::"."::: )  (Set (Var "i")) ")" ) ($#k6_domain_1 :::"}"::: ) ))))))) ; 
 
theorem :: YELLOW14:32 (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "M"))  (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k3_waybel18 :::"product"::: )  (Set  "(" (Set (Var "M"))  ($#k7_funcop_1 :::"-->"::: )  (Set (Var "T")) ")" ) ")" ) "holds"  (Bool (Set   ($#k5_card_3 :::"pi"::: )   "(" (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ")" ) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k2_pre_topc :::"Cl"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "(" (Set (Var "x"))  ($#k2_yellow14 :::"."::: )  (Set (Var "i")) ")" ) ($#k6_domain_1 :::"}"::: ) ))))))) ; 
 
theorem :: YELLOW14:33 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "X"))  "st" (Bool (Bool (Set (Var "f"))  ($#r1_funct_2 :::"="::: )  (Set   ($#k3_struct_0 :::"id"::: )  (Set (Var "X")))) & (Bool (Set (Var "g"))  ($#r1_funct_2 :::"="::: )  (Set   ($#k3_struct_0 :::"id"::: )  (Set (Var "X")))) & (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  )) "holds"  (Bool (Set   ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "X"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "Y"))) "," (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "Y"))) "#)" ))))) ; 
 
theorem :: YELLOW14:34 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y"))  "st" (Bool (Bool (Set   ($#k8_waybel18 :::"corestr"::: )  (Set (Var "f"))) "is"   ($#v5_pre_topc :::"continuous"::: )  )) "holds"  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ))) ; 
 registrationlet "X" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); let "Y" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Const "X")); 
cluster (Set   ($#k4_tmap_1 :::"incl"::: )  "Y") ->   ($#v5_pre_topc :::"continuous"::: )   ; 
end; 
theorem :: YELLOW14:35 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "T"))  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")))  ($#r2_funct_2 :::"="::: )  (Set (Var "f")))) "holds"  (Bool (Set (Set  "("  ($#k8_waybel18 :::"corestr"::: )  (Set (Var "f")) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "("  ($#k4_tmap_1 :::"incl"::: )  (Set  "("  ($#k7_waybel18 :::"Image"::: )  (Set (Var "f")) ")" ) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k3_struct_0 :::"id"::: )  (Set  "("  ($#k7_waybel18 :::"Image"::: )  (Set (Var "f")) ")" ))))) ; 
 
theorem :: YELLOW14:36 (Bool  "for" (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "W")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Var "Y")) "holds"  (Bool (Set   ($#k8_waybel18 :::"corestr"::: )  (Set  "("  ($#k4_tmap_1 :::"incl"::: )  (Set (Var "W")) ")" )) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ))) ; 
 
theorem :: YELLOW14:37 (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "being"   ($#v4_waybel_3 :::"non-Empty"::: )     ($#v1_waybel18 :::"TopStruct-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "M"))  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "M")) "holds"  (Bool (Set (Set (Var "J"))  ($#k4_waybel18 :::"."::: )  (Set (Var "i"))) "is"   ($#v6_pre_topc :::"T_0"::: )    ($#l1_pre_topc :::"TopSpace":::))  ")" )) "holds"  (Bool (Set   ($#k3_waybel18 :::"product"::: )  (Set (Var "J"))) "is"   ($#v6_pre_topc :::"T_0"::: )  ))) ; 
 registrationlet "I" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_pre_topc :::"T_0"::: )    ($#l1_pre_topc :::"TopSpace":::); 
cluster (Set   ($#k3_waybel18 :::"product"::: )  (Set  "(" "I"  ($#k7_funcop_1 :::"-->"::: )  "T" ")" )) ->   ($#v6_pre_topc :::"T_0"::: )   ; 
end; 
theorem :: YELLOW14:38 (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "being"   ($#v4_waybel_3 :::"non-Empty"::: )     ($#v1_waybel18 :::"TopStruct-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "M"))  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "M")) "holds"   (Bool  "("  (Bool (Set (Set (Var "J"))  ($#k4_waybel18 :::"."::: )  (Set (Var "i"))) "is"   ($#v7_pre_topc :::"T_1"::: )  ) & (Bool (Set (Set (Var "J"))  ($#k4_waybel18 :::"."::: )  (Set (Var "i"))) "is"   ($#v2_pre_topc :::"TopSpace-like"::: )  )  ")" )  ")" )) "holds"  (Bool (Set   ($#k3_waybel18 :::"product"::: )  (Set (Var "J"))) "is"   ($#v7_pre_topc :::"T_1"::: )  ))) ; 
 registrationlet "I" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v7_pre_topc :::"T_1"::: )    ($#l1_pre_topc :::"TopSpace":::); 
cluster (Set   ($#k3_waybel18 :::"product"::: )  (Set  "(" "I"  ($#k7_funcop_1 :::"-->"::: )  "T" ")" )) ->   ($#v7_pre_topc :::"T_1"::: )   ; 
end;