:: WAYBEL26  semantic presentation begin  notationlet "I" be    ($#m1_hidden :::"set"::: )  ; let "J" be   ($#v1_yellow_1 :::"RelStr-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); synonym "I" :::"-POS_prod"::: "J" for  :::"product"::: "J"; end; notationlet "I" be    ($#m1_hidden :::"set"::: )  ; let "J" be   ($#v4_waybel_3 :::"non-Empty"::: )     ($#v1_waybel18 :::"TopStruct-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); synonym "I" :::"-TOP_prod"::: "J" for  :::"product"::: "J"; end; definitionlet "X", "Y" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); func  :::"oContMaps":::  "(" "X" "," "Y" ")"  ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_orders_2 :::"strict"::: )     ($#l1_orders_2 :::"RelStr"::: )   equals :: WAYBEL26:def 1 (Set   ($#k3_waybel24 :::"ContMaps"::: )   "(" "X" "," (Set  "("  ($#k1_waybel25 :::"Omega"::: )  "Y" ")" ) ")" ); end; 






:: deftheorem    defines :::"oContMaps"::: WAYBEL26:def 1 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_waybel24 :::"ContMaps"::: )   "(" (Set (Var "X")) "," (Set  "("  ($#k1_waybel25 :::"Omega"::: )  (Set (Var "Y")) ")" ) ")" ))); 
 registrationlet "X", "Y" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); 
cluster (Set   ($#k1_waybel26 :::"oContMaps"::: )   "(" "X" "," "Y" ")" ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_monoid_0 :::"constituted-Functions"::: )     ($#v1_orders_2 :::"strict"::: )     ($#v3_orders_2 :::"reflexive"::: )     ($#v4_orders_2 :::"transitive"::: )   ; 
end; 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"::: )   )    ($#v6_pre_topc :::"T_0"::: )    ($#l1_pre_topc :::"TopSpace":::); 
cluster (Set   ($#k1_waybel26 :::"oContMaps"::: )   "(" "X" "," "Y" ")" ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_orders_2 :::"strict"::: )     ($#v5_orders_2 :::"antisymmetric"::: )   ; 
end; 
theorem :: WAYBEL26:1 (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 "a")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "a")) "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )) "iff" (Bool (Set (Var "a")) "is"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  "("  ($#k1_waybel25 :::"Omega"::: )  (Set (Var "Y")) ")" ))  ")" ))) ; 
 
theorem :: WAYBEL26:2 (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 "a")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "a")) "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )) "iff" (Bool (Set (Var "a")) "is"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")))  ")" ))) ; 
 
theorem :: WAYBEL26:3 (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 "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  "("  ($#k1_waybel25 :::"Omega"::: )  (Set (Var "Y")) ")" )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "f"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "g")))) "holds"  (Bool  "("  (Bool (Set (Var "a"))  ($#r3_orders_2 :::"<="::: )  (Set (Var "b"))) "iff" (Bool (Set (Var "f"))  ($#r1_yellow_2 :::"<="::: )  (Set (Var "g")))  ")" )))) ; 
 definitionlet "X", "Y" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); let "x" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); let "A" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Const "X")) "," (Set (Const "Y")) ")"  ")" ); :: original: :::"pi"::: redefine func  :::"pi":::  "(" "A" "," "x" ")"  ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_waybel25 :::"Omega"::: )  "Y" ")" ); end; registrationlet "X", "Y" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); let "x" be    ($#m1_hidden :::"set"::: )  ; let "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Const "X")) "," (Set (Const "Y")) ")"  ")" ); 
cluster (Set   ($#k5_card_3 :::"pi"::: )   "(" "A" "," "x" ")" ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: WAYBEL26:4 (Bool (Set   ($#k1_waybel25 :::"Omega"::: )  (Set  ($#k9_waybel18 :::"Sierpinski_Space"::: ) )) "is"    ($#m1_yellow_9 :::"TopAugmentation"::: )   "of" (Set   ($#k3_yellow_1 :::"BoolePoset"::: )  (Num 1))) ; 
 
theorem :: WAYBEL26:5 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k2_yellow_1 :::"InclPoset"::: )  (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "X"))) ")" ) "," (Set  "("  ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set  ($#k9_waybel18 :::"Sierpinski_Space"::: ) ) ")"  ")" ) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v23_waybel_0 :::"isomorphic"::: )  ) & (Bool  "("   "for" (Set (Var "V")) "being"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "V")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_funct_3 :::"chi"::: )   "(" (Set (Var "V")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) ")" ))  ")" )  ")" ))) ; 
 
theorem :: WAYBEL26:6 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k2_yellow_1 :::"InclPoset"::: )  (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "X")))) "," (Set   ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set  ($#k9_waybel18 :::"Sierpinski_Space"::: ) ) ")" )  ($#r5_waybel_1 :::"are_isomorphic"::: )  )) ; 
 definitionlet "X", "Y", "Z" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); let "f" be   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Const "Y")) "," (Set (Const "Z")); func  :::"oContMaps":::  "(" "X" "," "f" ")"  ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k1_waybel26 :::"oContMaps"::: )   "(" "X" "," "Y" ")"  ")" ) "," (Set  "("  ($#k1_waybel26 :::"oContMaps"::: )   "(" "X" "," "Z" ")"  ")" ) means :: WAYBEL26:def 2 (Bool  "for" (Set (Var "g")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" "X" "," "Y" "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set "f"  ($#k1_partfun1 :::"*"::: )  (Set (Var "g"))))); func  :::"oContMaps":::  "(" "f" "," "X" ")"  ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k1_waybel26 :::"oContMaps"::: )   "(" "Z" "," "X" ")"  ")" ) "," (Set  "("  ($#k1_waybel26 :::"oContMaps"::: )   "(" "Y" "," "X" ")"  ")" ) means :: WAYBEL26:def 3 (Bool  "for" (Set (Var "g")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" "Z" "," "X" "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k1_partfun1 :::"*"::: )  "f"))); end; 
















:: deftheorem    defines :::"oContMaps"::: WAYBEL26:def 2 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Z"))  (Bool  "for" (Set (Var "b5")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "," (Set  "("  ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "Z")) ")"  ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "f")) ")" )) "iff" (Bool  "for" (Set (Var "g")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds"  (Bool (Set (Set (Var "b5"))  ($#k1_funct_1 :::"."::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "g")))))  ")" )))); 
 
:: deftheorem    defines :::"oContMaps"::: WAYBEL26:def 3 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Z"))  (Bool  "for" (Set (Var "b5")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "Z")) "," (Set (Var "X")) ")"  ")" ) "," (Set  "("  ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "Y")) "," (Set (Var "X")) ")"  ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_waybel26 :::"oContMaps"::: )   "(" (Set (Var "f")) "," (Set (Var "X")) ")" )) "iff" (Bool  "for" (Set (Var "g")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Z")) "," (Set (Var "X")) "holds"  (Bool (Set (Set (Var "b5"))  ($#k1_funct_1 :::"."::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")))))  ")" )))); 
 
theorem :: WAYBEL26:7 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "Y")) "being"   ($#v1_waybel25 :::"monotone-convergence"::: )    ($#l1_pre_topc :::"T_0-TopSpace":::) "holds"  (Bool (Set   ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) "is"   ($#v24_waybel_0 :::"up-complete"::: )  ))) ; 
 
theorem :: WAYBEL26:8 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) "holds"  (Bool (Set   ($#k3_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "f")) ")" ) "is"   ($#v5_orders_3 :::"monotone"::: )  ))) ; 
 
theorem :: WAYBEL26:9 (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"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Y"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v11_quantal1 :::"idempotent"::: )  )) "holds"  (Bool (Set   ($#k3_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "f")) ")" ) "is"   ($#v11_quantal1 :::"idempotent"::: )  ))) ; 
 
theorem :: WAYBEL26:10 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) "holds"  (Bool (Set   ($#k4_waybel26 :::"oContMaps"::: )   "(" (Set (Var "f")) "," (Set (Var "X")) ")" ) "is"   ($#v5_orders_3 :::"monotone"::: )  ))) ; 
 
theorem :: WAYBEL26:11 (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"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Y"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v11_quantal1 :::"idempotent"::: )  )) "holds"  (Bool (Set   ($#k4_waybel26 :::"oContMaps"::: )   "(" (Set (Var "f")) "," (Set (Var "X")) ")" ) "is"   ($#v11_quantal1 :::"idempotent"::: )  ))) ; 
 
theorem :: WAYBEL26:12 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Z"))  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "holds"  (Bool (Set   ($#k2_waybel26 :::"pi"::: )   "(" (Set  "(" (Set  "("  ($#k3_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "f")) ")"  ")" )  ($#k7_relset_1 :::".:"::: )  (Set (Var "A")) ")" ) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set  "("  ($#k2_waybel26 :::"pi"::: )   "(" (Set (Var "A")) "," (Set (Var "x")) ")"  ")" ))))))) ; 
 
theorem :: WAYBEL26:13 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "Y")) "," (Set (Var "Z")) "being"   ($#v1_waybel25 :::"monotone-convergence"::: )    ($#l1_pre_topc :::"T_0-TopSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) "holds"  (Bool (Set   ($#k3_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "f")) ")" ) "is"   ($#v22_waybel_0 :::"directed-sups-preserving"::: )  )))) ; 
 
theorem :: WAYBEL26:14 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Z"))  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Y"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "Z")) "," (Set (Var "X")) ")"  ")" ) "holds"  (Bool (Set   ($#k2_waybel26 :::"pi"::: )   "(" (Set  "(" (Set  "("  ($#k4_waybel26 :::"oContMaps"::: )   "(" (Set (Var "f")) "," (Set (Var "X")) ")"  ")" )  ($#k7_relset_1 :::".:"::: )  (Set (Var "A")) ")" ) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k2_waybel26 :::"pi"::: )   "(" (Set (Var "A")) "," (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" ) ")" )))))) ; 
 
theorem :: WAYBEL26:15 (Bool  "for" (Set (Var "Y")) "," (Set (Var "Z")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "X")) "being"   ($#v1_waybel25 :::"monotone-convergence"::: )    ($#l1_pre_topc :::"T_0-TopSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) "holds"  (Bool (Set   ($#k4_waybel26 :::"oContMaps"::: )   "(" (Set (Var "f")) "," (Set (Var "X")) ")" ) "is"   ($#v22_waybel_0 :::"directed-sups-preserving"::: )  )))) ; 
 
theorem :: WAYBEL26:16 (Bool  "for" (Set (Var "X")) "," (Set (Var "Z")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Var "Z")) "holds"  (Bool (Set   ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) "is"   ($#v4_yellow_0 :::"full"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set   ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "Z")) ")" )))) ; 
 
theorem :: WAYBEL26:17 (Bool  "for" (Set (Var "Z")) "being"   ($#v1_waybel25 :::"monotone-convergence"::: )    ($#l1_pre_topc :::"T_0-TopSpace":::)  (Bool  "for" (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Var "Z"))  (Bool  "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Z")) "," (Set (Var "Y"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v3_borsuk_1 :::"being_a_retraction"::: )  )) "holds"  (Bool (Set   ($#k1_waybel25 :::"Omega"::: )  (Set (Var "Y"))) "is"   ($#v4_waybel_0 :::"directed-sups-inheriting"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set   ($#k1_waybel25 :::"Omega"::: )  (Set (Var "Z"))))))) ; 
 
theorem :: WAYBEL26:18 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v1_waybel25 :::"monotone-convergence"::: )    ($#l1_pre_topc :::"T_0-TopSpace":::)  (Bool  "for" (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Var "Z"))  (Bool  "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Z")) "," (Set (Var "Y"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v3_borsuk_1 :::"being_a_retraction"::: )  )) "holds"  (Bool (Set   ($#k3_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "f")) ")" )  ($#r1_yellow16 :::"is_a_retraction_of"::: )  (Set   ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "Z")) ")" ) "," (Set   ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )))))) ; 
 
theorem :: WAYBEL26:19 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v1_waybel25 :::"monotone-convergence"::: )    ($#l1_pre_topc :::"T_0-TopSpace":::)  (Bool  "for" (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Var "Z"))  "st" (Bool (Bool (Set (Var "Y"))  ($#r1_borsuk_1 :::"is_a_retract_of"::: )  (Set (Var "Z")))) "holds"  (Bool (Set   ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )  ($#r3_yellow16 :::"is_a_retract_of"::: )  (Set   ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "Z")) ")" ))))) ; 
 
theorem :: WAYBEL26:20 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Z"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  )) "holds"  (Bool (Set   ($#k3_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "f")) ")" ) "is"   ($#v23_waybel_0 :::"isomorphic"::: )  ))) ; 
 
theorem :: WAYBEL26:21 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Set (Var "Y")) "," (Set (Var "Z"))  ($#r1_t_0topsp :::"are_homeomorphic"::: )  )) "holds"  (Bool (Set   ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) "," (Set   ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "Z")) ")" )  ($#r5_waybel_1 :::"are_isomorphic"::: )  )) ; 
 
theorem :: WAYBEL26:22 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v1_waybel25 :::"monotone-convergence"::: )    ($#l1_pre_topc :::"T_0-TopSpace":::)  (Bool  "for" (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Var "Z"))  "st" (Bool (Bool (Set (Var "Y"))  ($#r1_borsuk_1 :::"is_a_retract_of"::: )  (Set (Var "Z"))) & (Bool (Set   ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "Z")) ")" ) "is"   ($#v3_lattice3 :::"complete"::: )  ) & (Bool (Set   ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "Z")) ")" ) "is"   ($#v3_waybel_3 :::"continuous"::: )  )) "holds"  (Bool  "("  (Bool (Set   ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) "is"   ($#v3_lattice3 :::"complete"::: )  ) & (Bool (Set   ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) "is"   ($#v3_waybel_3 :::"continuous"::: )  )  ")" )))) ; 
 
theorem :: WAYBEL26:23 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "Y")) "," (Set (Var "Z")) "being"   ($#v1_waybel25 :::"monotone-convergence"::: )    ($#l1_pre_topc :::"T_0-TopSpace":::)  "st" (Bool (Bool (Set (Var "Y"))  ($#r1_waybel18 :::"is_Retract_of"::: )  (Set (Var "Z"))) & (Bool (Set   ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "Z")) ")" ) "is"   ($#v3_lattice3 :::"complete"::: )  ) & (Bool (Set   ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "Z")) ")" ) "is"   ($#v3_waybel_3 :::"continuous"::: )  )) "holds"  (Bool  "("  (Bool (Set   ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) "is"   ($#v3_lattice3 :::"complete"::: )  ) & (Bool (Set   ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) "is"   ($#v3_waybel_3 :::"continuous"::: )  )  ")" ))) ; 
 
theorem :: WAYBEL26:24 (Bool  "for" (Set (Var "Y")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_pre_topc :::"T_0-TopSpace":::)  "st" (Bool (Bool (Bool  "not" (Set (Var "Y")) "is"   ($#v7_pre_topc :::"T_1"::: )  ))) "holds"  (Bool (Set   ($#k9_waybel18 :::"Sierpinski_Space"::: )  )  ($#r1_waybel18 :::"is_Retract_of"::: )  (Set (Var "Y")))) ; 
 
theorem :: WAYBEL26:25 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "Y")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )   ($#l1_pre_topc :::"T_0-TopSpace":::)  "st" (Bool (Bool (Set   ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) "is"   ($#v1_lattice3 :::"with_suprema"::: )  )) "holds"  (Bool  "not" (Bool (Set (Var "Y")) "is"   ($#v7_pre_topc :::"T_1"::: )  )))) ; 
 registration
cluster (Set   ($#k9_waybel18 :::"Sierpinski_Space"::: )  ) ->  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )    ($#v1_waybel25 :::"monotone-convergence"::: )   ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )    ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v6_pre_topc :::"T_0"::: )     ($#v2_waybel18 :::"injective"::: )     ($#v1_waybel25 :::"monotone-convergence"::: )    for    ($#l1_pre_topc :::"TopStruct"::: )  ; 
end; 
theorem :: WAYBEL26:26 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "Y")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )    ($#v1_waybel25 :::"monotone-convergence"::: )    ($#l1_pre_topc :::"T_0-TopSpace":::)  "st" (Bool (Bool (Set   ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) "is"   ($#v3_lattice3 :::"complete"::: )  ) & (Bool (Set   ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) "is"   ($#v3_waybel_3 :::"continuous"::: )  )) "holds"  (Bool (Set   ($#k2_yellow_1 :::"InclPoset"::: )  (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "X")))) "is"   ($#v3_waybel_3 :::"continuous"::: )  ))) ; 
 
theorem :: WAYBEL26:27 (Bool  "for" (Set (Var "X")) "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 (Var "X"))  (Bool  "for" (Set (Var "Y")) "being"   ($#v1_waybel25 :::"monotone-convergence"::: )    ($#l1_pre_topc :::"T_0-TopSpace":::) (Bool  "ex" (Set (Var "F")) "being"   ($#v22_waybel_0 :::"directed-sups-preserving"::: )     ($#v6_waybel_1 :::"projection"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "," (Set  "("  ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "st"  (Bool  "("  (Bool  "("   "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds"  (Bool (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k6_struct_0 :::"-->"::: )  (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" )))  ")" ) & (Bool  "ex" (Set (Var "h")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X")) "st"  (Bool  "("  (Bool (Set (Var "h"))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "X"))  ($#k6_struct_0 :::"-->"::: )  (Set (Var "x")))) & (Bool (Set (Var "F"))  ($#r2_funct_2 :::"="::: )  (Set   ($#k4_waybel26 :::"oContMaps"::: )   "(" (Set (Var "h")) "," (Set (Var "Y")) ")" ))  ")" ))  ")" ))))) ; 
 
theorem :: WAYBEL26:28 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "Y")) "being"   ($#v1_waybel25 :::"monotone-convergence"::: )    ($#l1_pre_topc :::"T_0-TopSpace":::)  "st" (Bool (Bool (Set   ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) "is"   ($#v3_lattice3 :::"complete"::: )  ) & (Bool (Set   ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) "is"   ($#v3_waybel_3 :::"continuous"::: )  )) "holds"  (Bool  "("  (Bool (Set   ($#k1_waybel25 :::"Omega"::: )  (Set (Var "Y"))) "is"   ($#v3_lattice3 :::"complete"::: )  ) & (Bool (Set   ($#k1_waybel25 :::"Omega"::: )  (Set (Var "Y"))) "is"   ($#v3_waybel_3 :::"continuous"::: )  )  ")" ))) ; 
 
theorem :: WAYBEL26:29 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "I")) "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 "I"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  "(" (Set (Var "I"))  ($#k3_waybel18 :::"-TOP_prod"::: )  (Set (Var "J")) ")" )  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I")) "holds"  (Bool (Set (Set  "("  ($#k10_funct_6 :::"commute"::: )  (Set (Var "f")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_waybel18 :::"proj"::: )   "(" (Set (Var "J")) "," (Set (Var "i")) ")"  ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f"))))))))) ; 
 
theorem :: WAYBEL26:30 (Bool  "for" (Set (Var "S")) "being"    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "M")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k12_pralg_1 :::"Carrier"::: )  (Set  "(" (Set (Var "M"))  ($#k7_funcop_1 :::"-->"::: )  (Set (Var "S")) ")" ))  ($#r6_pboole :::"="::: )  (Set (Set (Var "M"))  ($#k7_funcop_1 :::"-->"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))))))) ; 
 
theorem :: WAYBEL26:31 (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 "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  "(" (Set (Var "M"))  ($#k3_waybel18 :::"-TOP_prod"::: )  (Set  "(" (Set (Var "M"))  ($#k7_funcop_1 :::"-->"::: )  (Set (Var "Y")) ")" ) ")" ) "holds"  (Bool (Set   ($#k10_funct_6 :::"commute"::: )  (Set (Var "f"))) "is"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "M")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )))))) ; 
 
theorem :: WAYBEL26:32 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "Y"))) ")" ))) ; 
 
theorem :: WAYBEL26:33 (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 "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "M")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )) "holds"  (Bool (Set   ($#k10_funct_6 :::"commute"::: )  (Set (Var "f"))) "is"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  "(" (Set (Var "M"))  ($#k3_waybel18 :::"-TOP_prod"::: )  (Set  "(" (Set (Var "M"))  ($#k7_funcop_1 :::"-->"::: )  (Set (Var "Y")) ")" ) ")" ))))) ; 
 
theorem :: WAYBEL26:34 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   (Bool  "ex" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set  "(" (Set (Var "M"))  ($#k3_waybel18 :::"-TOP_prod"::: )  (Set  "(" (Set (Var "M"))  ($#k7_funcop_1 :::"-->"::: )  (Set  ($#k9_waybel18 :::"Sierpinski_Space"::: ) ) ")" ) ")" ) ")"  ")" ) "," (Set  "(" (Set (Var "M"))  ($#k5_yellow_1 :::"-POS_prod"::: )  (Set  "(" (Set (Var "M"))  ($#k7_funcop_1 :::"-->"::: )  (Set  "("  ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set  ($#k9_waybel18 :::"Sierpinski_Space"::: ) ) ")"  ")" ) ")" ) ")" ) "st"  (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v23_waybel_0 :::"isomorphic"::: )  ) & (Bool  "("   "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  "(" (Set (Var "M"))  ($#k3_waybel18 :::"-TOP_prod"::: )  (Set  "(" (Set (Var "M"))  ($#k7_funcop_1 :::"-->"::: )  (Set  ($#k9_waybel18 :::"Sierpinski_Space"::: ) ) ")" ) ")" ) "holds"  (Bool (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k10_funct_6 :::"commute"::: )  (Set (Var "f"))))  ")" )  ")" )))) ; 
 
theorem :: WAYBEL26:35 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set  "(" (Set (Var "M"))  ($#k3_waybel18 :::"-TOP_prod"::: )  (Set  "(" (Set (Var "M"))  ($#k7_funcop_1 :::"-->"::: )  (Set  ($#k9_waybel18 :::"Sierpinski_Space"::: ) ) ")" ) ")" ) ")" ) "," (Set (Set (Var "M"))  ($#k5_yellow_1 :::"-POS_prod"::: )  (Set  "(" (Set (Var "M"))  ($#k7_funcop_1 :::"-->"::: )  (Set  "("  ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set  ($#k9_waybel18 :::"Sierpinski_Space"::: ) ) ")"  ")" ) ")" ))  ($#r5_waybel_1 :::"are_isomorphic"::: )  ))) ; 
 
theorem :: WAYBEL26:36 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Set   ($#k2_yellow_1 :::"InclPoset"::: )  (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "X")))) "is"   ($#v3_waybel_3 :::"continuous"::: )  )) "holds"  (Bool  "for" (Set (Var "Y")) "being"   ($#v2_waybel18 :::"injective"::: )    ($#l1_pre_topc :::"T_0-TopSpace":::) "holds"   (Bool  "("  (Bool (Set   ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) "is"   ($#v3_lattice3 :::"complete"::: )  ) & (Bool (Set   ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) "is"   ($#v3_waybel_3 :::"continuous"::: )  )  ")" ))) ; 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )    ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v3_orders_2 :::"reflexive"::: )     ($#v4_orders_2 :::"transitive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v1_lattice3 :::"with_suprema"::: )     ($#v2_lattice3 :::"with_infima"::: )     ($#v3_lattice3 :::"complete"::: )     ($#v4_waybel11 :::"Scott"::: )    for    ($#l1_waybel_9 :::"TopRelStr"::: )  ; 
end; 
theorem :: WAYBEL26:37 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "L")) "being"  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )    ($#v3_lattice3 :::"complete"::: )     ($#v4_waybel11 :::"Scott"::: )    ($#l1_waybel_9 :::"TopLattice":::) "holds"   (Bool  "("  (Bool (Set   ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "L")) ")" ) "is"   ($#v3_lattice3 :::"complete"::: )  ) & (Bool (Set   ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "L")) ")" ) "is"   ($#v3_waybel_3 :::"continuous"::: )  ) "iff" (Bool  "("  (Bool (Set   ($#k2_yellow_1 :::"InclPoset"::: )  (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "X")))) "is"   ($#v3_waybel_3 :::"continuous"::: )  ) & (Bool (Set (Var "L")) "is"   ($#v3_waybel_3 :::"continuous"::: )  )  ")" )  ")" ))) ; 
 registrationlet "f" be   ($#m1_hidden :::"Function":::); 
cluster (Set   ($#k3_card_3 :::"Union"::: )  (Set  "("  ($#k2_card_3 :::"disjoin"::: )  "f" ")" )) ->   ($#v1_relat_1 :::"Relation-like"::: )   ; 
end; definitionlet "f" be   ($#m1_hidden :::"Function":::); func  :::"*graph"::: "f" ->   ($#m1_hidden :::"Relation":::) equals :: WAYBEL26:def 4 (Set (Set  "("  ($#k3_card_3 :::"Union"::: )  (Set  "("  ($#k2_card_3 :::"disjoin"::: )  "f" ")" ) ")" )  ($#k2_relat_1 :::"~"::: )  ); end; 





:: deftheorem    defines :::"*graph"::: WAYBEL26:def 4 :  (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"  (Bool (Set   ($#k5_waybel26 :::"*graph"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_card_3 :::"Union"::: )  (Set  "("  ($#k2_card_3 :::"disjoin"::: )  (Set (Var "f")) ")" ) ")" )  ($#k2_relat_1 :::"~"::: )  ))); 
 







theorem :: WAYBEL26:38 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k5_waybel26 :::"*graph"::: )  (Set (Var "f")))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x"))))  ")" )  ")" ))) ; 
 
theorem :: WAYBEL26:39 (Bool  "for" (Set (Var "X")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"proj1"::: )  (Set (Var "X"))) "is"   ($#v1_finset_1 :::"finite"::: )  ) & (Bool (Set   ($#k10_xtuple_0 :::"proj2"::: )  (Set (Var "X"))) "is"   ($#v1_finset_1 :::"finite"::: )  )  ")" )) ; 
 
theorem :: WAYBEL26:40 (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 "S")) "being"   ($#v4_waybel11 :::"Scott"::: )     ($#m1_yellow_9 :::"TopAugmentation"::: )   "of" (Set   ($#k2_yellow_1 :::"InclPoset"::: )  (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "Y"))))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "S"))  "st" (Bool (Bool (Set   ($#k5_waybel26 :::"*graph"::: )  (Set (Var "f"))) "is"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_borsuk_1 :::":]"::: ) ))) "holds"  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  )))) ; 
 definitionlet "W" be   ($#m1_hidden :::"Relation":::); let "X" be    ($#m1_hidden :::"set"::: )  ; func  "(" "W" "," "X" ")"  :::"*graph":::  ->   ($#m1_hidden :::"Function":::) means :: WAYBEL26:def 5 (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  it)  ($#r1_hidden :::"="::: )  "X") & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "X")) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k9_relat_1 :::"Im"::: )   "(" "W" "," (Set (Var "x")) ")" ))  ")" )  ")" ); end; 






:: deftheorem    defines :::"*graph"::: WAYBEL26:def 5 :  (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Relation":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b3")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set  "(" (Set (Var "W")) "," (Set (Var "X")) ")"   ($#k6_waybel26 :::"*graph"::: )  )) "iff" (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set (Var "X"))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Set (Var "b3"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k9_relat_1 :::"Im"::: )   "(" (Set (Var "W")) "," (Set (Var "x")) ")" ))  ")" )  ")" )  ")" )))); 
 
theorem :: WAYBEL26:41 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Relation":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "W")))  ($#r1_tarski :::"c="::: )  (Set (Var "X")))) "holds"  (Bool (Set   ($#k5_waybel26 :::"*graph"::: )  (Set  "("  "(" (Set (Var "W")) "," (Set (Var "X")) ")"   ($#k6_waybel26 :::"*graph"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "W"))))) ; 
 registrationlet "X", "Y" be   ($#l1_pre_topc :::"TopSpace":::); 
cluster   ->   ($#v1_relat_1 :::"Relation-like"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) "X" "," "Y" ($#k2_borsuk_1 :::":]"::: ) ))); 

cluster   ->   ($#v1_relat_1 :::"Relation-like"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) "X" "," "Y" ($#k2_borsuk_1 :::":]"::: ) )); 
end; 
theorem :: WAYBEL26:42 (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 "W")) "being"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_borsuk_1 :::":]"::: ) )  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k9_relat_1 :::"Im"::: )   "(" (Set (Var "W")) "," (Set (Var "x")) ")" ) "is"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")))))) ; 
 
theorem :: WAYBEL26:43 (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 "S")) "being"   ($#v4_waybel11 :::"Scott"::: )     ($#m1_yellow_9 :::"TopAugmentation"::: )   "of" (Set   ($#k2_yellow_1 :::"InclPoset"::: )  (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "Y"))))  (Bool  "for" (Set (Var "W")) "being"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_borsuk_1 :::":]"::: ) ) "holds"  (Bool (Set  "(" (Set (Var "W")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) ")"   ($#k6_waybel26 :::"*graph"::: )  ) "is"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "S")))))) ; 
 
theorem :: WAYBEL26:44 (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 "S")) "being"   ($#v4_waybel11 :::"Scott"::: )     ($#m1_yellow_9 :::"TopAugmentation"::: )   "of" (Set   ($#k2_yellow_1 :::"InclPoset"::: )  (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "Y"))))  (Bool  "for" (Set (Var "W1")) "," (Set (Var "W2")) "being"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_borsuk_1 :::":]"::: ) )  "st" (Bool (Bool (Set (Var "W1"))  ($#r1_tarski :::"c="::: )  (Set (Var "W2")))) "holds"  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "S")) ")"  ")" )  "st" (Bool (Bool (Set (Var "f1"))  ($#r1_hidden :::"="::: )  (Set  "(" (Set (Var "W1")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) ")"   ($#k6_waybel26 :::"*graph"::: )  )) & (Bool (Set (Var "f2"))  ($#r1_hidden :::"="::: )  (Set  "(" (Set (Var "W2")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) ")"   ($#k6_waybel26 :::"*graph"::: )  ))) "holds"  (Bool (Set (Var "f1"))  ($#r3_orders_2 :::"<="::: )  (Set (Var "f2"))))))) ; 
 
theorem :: WAYBEL26:45 (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 "S")) "being"   ($#v4_waybel11 :::"Scott"::: )     ($#m1_yellow_9 :::"TopAugmentation"::: )   "of" (Set   ($#k2_yellow_1 :::"InclPoset"::: )  (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "Y")))) (Bool  "ex" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k2_yellow_1 :::"InclPoset"::: )  (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_borsuk_1 :::":]"::: ) )) ")" ) "," (Set  "("  ($#k1_waybel26 :::"oContMaps"::: )   "(" (Set (Var "X")) "," (Set (Var "S")) ")"  ")" ) "st"  (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v5_orders_3 :::"monotone"::: )  ) & (Bool  "("   "for" (Set (Var "W")) "being"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_borsuk_1 :::":]"::: ) ) "holds"  (Bool (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "W")))  ($#r1_hidden :::"="::: )  (Set  "(" (Set (Var "W")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) ")"   ($#k6_waybel26 :::"*graph"::: )  ))  ")" )  ")" )))) ;