:: YELLOW12  semantic presentation begin  





registrationlet "X" be   ($#v1_xboole_0 :::"empty"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k3_tarski :::"union"::: )  "X") ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; 
theorem :: YELLOW12:1 (Bool  "for" (Set (Var "X")) "," (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  "("  ($#k12_funct_3 :::"delta"::: )  (Set (Var "X")) ")" )  ($#k7_relset_1 :::".:"::: )  (Set (Var "A")))  ($#r1_relset_1 :::"c="::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k2_zfmisc_1 :::":]"::: ) ))) ; 
 
theorem :: YELLOW12:2 (Bool  "for" (Set (Var "X")) "," (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  "("  ($#k12_funct_3 :::"delta"::: )  (Set (Var "X")) ")" )  ($#k8_relset_1 :::"""::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k2_zfmisc_1 :::":]"::: ) ))  ($#r1_tarski :::"c="::: )  (Set (Var "A")))) ; 
 
theorem :: YELLOW12:3 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set  "("  ($#k12_funct_3 :::"delta"::: )  (Set (Var "X")) ")" )  ($#k8_relset_1 :::"""::: )  (Set  ($#k8_mcart_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k8_mcart_1 :::":]"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "A"))))) ; 
 
theorem :: YELLOW12:4 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  ($#k13_funct_3 :::"<:"::: ) (Set  "("  ($#k10_funct_3 :::"pr2"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "," (Set  "("  ($#k9_funct_3 :::"pr1"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) ($#k13_funct_3 :::":>"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  ($#k13_funct_3 :::"<:"::: ) (Set  "("  ($#k10_funct_3 :::"pr2"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "," (Set  "("  ($#k9_funct_3 :::"pr1"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) ($#k13_funct_3 :::":>"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ))  ")" )) ; 
 
theorem :: YELLOW12:5 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  ($#k13_funct_3 :::"<:"::: ) (Set  "("  ($#k10_funct_3 :::"pr2"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "," (Set  "("  ($#k9_funct_3 :::"pr1"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) ($#k13_funct_3 :::":>"::: ) )  ($#k7_relat_1 :::".:"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ))  ($#r1_tarski :::"c="::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "B")) "," (Set (Var "A")) ($#k2_zfmisc_1 :::":]"::: ) ))) ; 
 
theorem :: YELLOW12:6 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "holds"  (Bool (Set (Set  ($#k13_funct_3 :::"<:"::: ) (Set  "("  ($#k10_funct_3 :::"pr2"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "," (Set  "("  ($#k9_funct_3 :::"pr1"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) ($#k13_funct_3 :::":>"::: ) )  ($#k7_relat_1 :::".:"::: )  (Set  ($#k8_mcart_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k8_mcart_1 :::":]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k8_mcart_1 :::"[:"::: ) (Set (Var "B")) "," (Set (Var "A")) ($#k8_mcart_1 :::":]"::: ) ))))) ; 
 
theorem :: YELLOW12:7 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set  ($#k13_funct_3 :::"<:"::: ) (Set  "("  ($#k10_funct_3 :::"pr2"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "," (Set  "("  ($#k9_funct_3 :::"pr1"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) ($#k13_funct_3 :::":>"::: ) ) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )) ; 
 registrationlet "X", "Y" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set  ($#k13_funct_3 :::"<:"::: ) (Set  "("  ($#k10_funct_3 :::"pr2"::: )   "(" "X" "," "Y" ")"  ")" ) "," (Set  "("  ($#k9_funct_3 :::"pr1"::: )   "(" "X" "," "Y" ")"  ")" ) ($#k13_funct_3 :::":>"::: ) ) ->   ($#v2_funct_1 :::"one-to-one"::: )   ; 
end; 
theorem :: YELLOW12:8 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  ($#k13_funct_3 :::"<:"::: ) (Set  "("  ($#k10_funct_3 :::"pr2"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "," (Set  "("  ($#k9_funct_3 :::"pr1"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) ($#k13_funct_3 :::":>"::: ) )  ($#k2_funct_1 :::"""::: )  )  ($#r1_hidden :::"="::: )  (Set  ($#k13_funct_3 :::"<:"::: ) (Set  "("  ($#k10_funct_3 :::"pr2"::: )   "(" (Set (Var "Y")) "," (Set (Var "X")) ")"  ")" ) "," (Set  "("  ($#k9_funct_3 :::"pr1"::: )   "(" (Set (Var "Y")) "," (Set (Var "X")) ")"  ")" ) ($#k13_funct_3 :::":>"::: ) ))) ; 
 begin  
theorem :: YELLOW12:9 (Bool  "for" (Set (Var "L1")) "being"   ($#l1_orders_2 :::"Semilattice":::)  (Bool  "for" (Set (Var "L2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1"))  (Bool  "for" (Set (Var "x1")) "," (Set (Var "y1")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L2"))  "st" (Bool (Bool (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L1"))) "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "L1"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L2"))) "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "L2"))) "#)" )) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "x1"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "y1")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k12_lattice3 :::""/\""::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x1"))  ($#k11_lattice3 :::""/\""::: )  (Set (Var "y1")))))))) ; 
 
theorem :: YELLOW12:10 (Bool  "for" (Set (Var "L1")) "being"   ($#l1_orders_2 :::"sup-Semilattice":::)  (Bool  "for" (Set (Var "L2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1"))  (Bool  "for" (Set (Var "x1")) "," (Set (Var "y1")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L2"))  "st" (Bool (Bool (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L1"))) "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "L1"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L2"))) "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "L2"))) "#)" )) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "x1"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "y1")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k13_lattice3 :::""\/""::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x1"))  ($#k10_lattice3 :::""\/""::: )  (Set (Var "y1")))))))) ; 
 
theorem :: YELLOW12:11 (Bool  "for" (Set (Var "L1")) "being"   ($#l1_orders_2 :::"Semilattice":::)  (Bool  "for" (Set (Var "L2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L1"))  (Bool  "for" (Set (Var "X1")) "," (Set (Var "Y1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L2"))  "st" (Bool (Bool (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L1"))) "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "L1"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L2"))) "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "L2"))) "#)" )) & (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set (Var "X1"))) & (Bool (Set (Var "Y"))  ($#r1_hidden :::"="::: )  (Set (Var "Y1")))) "holds"  (Bool (Set (Set (Var "X"))  ($#k4_yellow_4 :::""/\""::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X1"))  ($#k3_yellow_4 :::""/\""::: )  (Set (Var "Y1")))))))) ; 
 
theorem :: YELLOW12:12 (Bool  "for" (Set (Var "L1")) "being"   ($#l1_orders_2 :::"sup-Semilattice":::)  (Bool  "for" (Set (Var "L2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L1"))  (Bool  "for" (Set (Var "X1")) "," (Set (Var "Y1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L2"))  "st" (Bool (Bool (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L1"))) "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "L1"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L2"))) "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "L2"))) "#)" )) & (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set (Var "X1"))) & (Bool (Set (Var "Y"))  ($#r1_hidden :::"="::: )  (Set (Var "Y1")))) "holds"  (Bool (Set (Set (Var "X"))  ($#k2_yellow_4 :::""\/""::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X1"))  ($#k1_yellow_4 :::""\/""::: )  (Set (Var "Y1")))))))) ; 
 
theorem :: YELLOW12:13 (Bool  "for" (Set (Var "L1")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v24_waybel_0 :::"up-complete"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "L2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1"))  (Bool  "for" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L2"))  "st" (Bool (Bool (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L1"))) "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "L1"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L2"))) "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "L2"))) "#)" )) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y")))) "holds"  (Bool  "("  (Bool (Set   ($#k1_waybel_3 :::"waybelow"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_waybel_3 :::"waybelow"::: )  (Set (Var "y")))) & (Bool (Set   ($#k2_waybel_3 :::"wayabove"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_waybel_3 :::"wayabove"::: )  (Set (Var "y"))))  ")" ))))) ; 
 
theorem :: YELLOW12:14 (Bool  "for" (Set (Var "L1")) "being"   ($#v2_waybel_2 :::"meet-continuous"::: )    ($#l1_orders_2 :::"Semilattice":::)  (Bool  "for" (Set (Var "L2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#l1_orders_2 :::"RelStr"::: )    "st" (Bool (Bool (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L1"))) "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "L1"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L2"))) "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "L2"))) "#)" ))) "holds"  (Bool (Set (Var "L2")) "is"   ($#v2_waybel_2 :::"meet-continuous"::: )  ))) ; 
 
theorem :: YELLOW12:15 (Bool  "for" (Set (Var "L1")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v3_waybel_3 :::"continuous"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "L2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#l1_orders_2 :::"RelStr"::: )    "st" (Bool (Bool (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L1"))) "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "L1"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L2"))) "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "L2"))) "#)" ))) "holds"  (Bool (Set (Var "L2")) "is"   ($#v3_waybel_3 :::"continuous"::: )  ))) ; 
 
theorem :: YELLOW12:16 (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L1"))  (Bool  "for" (Set (Var "J")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L2"))  "st" (Bool (Bool (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L1"))) "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "L1"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L2"))) "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "L2"))) "#)" )) & (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Var "J")))) "holds"  (Bool (Set   ($#k5_yellow_0 :::"subrelstr"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_yellow_0 :::"subrelstr"::: )  (Set (Var "J"))))))) ; 
 
theorem :: YELLOW12:17 (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "A")) "being"    ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set (Var "L1"))  (Bool  "for" (Set (Var "J")) "being"    ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set (Var "L2"))  "st" (Bool (Bool (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L1"))) "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "L1"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L2"))) "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "L2"))) "#)" )) & (Bool (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "A"))) "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "A"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "J"))) "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "J"))) "#)" )) & (Bool (Set (Var "A")) "is"   ($#v5_yellow_0 :::"meet-inheriting"::: )  )) "holds"  (Bool (Set (Var "J")) "is"   ($#v5_yellow_0 :::"meet-inheriting"::: )  )))) ; 
 
theorem :: YELLOW12:18 (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "A")) "being"    ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set (Var "L1"))  (Bool  "for" (Set (Var "J")) "being"    ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set (Var "L2"))  "st" (Bool (Bool (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L1"))) "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "L1"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L2"))) "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "L2"))) "#)" )) & (Bool (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "A"))) "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "A"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "J"))) "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "J"))) "#)" )) & (Bool (Set (Var "A")) "is"   ($#v6_yellow_0 :::"join-inheriting"::: )  )) "holds"  (Bool (Set (Var "J")) "is"   ($#v6_yellow_0 :::"join-inheriting"::: )  )))) ; 
 
theorem :: YELLOW12:19 (Bool  "for" (Set (Var "L1")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v24_waybel_0 :::"up-complete"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "L2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L1"))  (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L2"))  "st" (Bool (Bool (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L1"))) "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "L1"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L2"))) "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "L2"))) "#)" )) & (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set (Var "Y"))) & (Bool (Set (Var "X")) "is"   ($#v3_waybel11 :::"property(S)"::: )  )) "holds"  (Bool (Set (Var "Y")) "is"   ($#v3_waybel11 :::"property(S)"::: )  ))))) ; 
 
theorem :: YELLOW12:20 (Bool  "for" (Set (Var "L1")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v24_waybel_0 :::"up-complete"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "L2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L1"))  (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L2"))  "st" (Bool (Bool (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L1"))) "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "L1"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L2"))) "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "L2"))) "#)" )) & (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set (Var "Y"))) & (Bool (Set (Var "X")) "is"   ($#v2_waybel11 :::"directly_closed"::: )  )) "holds"  (Bool (Set (Var "Y")) "is"   ($#v2_waybel11 :::"directly_closed"::: )  ))))) ; 
 
theorem :: YELLOW12:21 (Bool  "for" (Set (Var "N")) "being"   ($#v5_orders_2 :::"antisymmetric"::: )     ($#v2_lattice3 :::"with_infima"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "D")) "," (Set (Var "E")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N"))  (Bool  "for" (Set (Var "X")) "being"   ($#v13_waybel_0 :::"upper"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N"))  "st" (Bool (Bool (Set (Var "D"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Set (Var "D"))  ($#k4_yellow_4 :::""/\""::: )  (Set (Var "E")))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "X")))))) ; 
 
theorem :: YELLOW12:22 (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#l1_orders_2 :::"RelStr"::: )   "holds"  (Bool (Set   ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R"))))  ($#r1_relset_1 :::"c="::: )  (Set (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "R")))  ($#k9_subset_1 :::"/\"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set  "(" (Set (Var "R"))  ($#k7_lattice3 :::"~"::: )  ")" ))))) ; 
 
theorem :: YELLOW12:23 (Bool  "for" (Set (Var "R")) "being"   ($#v5_orders_2 :::"antisymmetric"::: )     ($#l1_orders_2 :::"RelStr"::: )   "holds"  (Bool (Set (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "R")))  ($#k9_subset_1 :::"/\"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set  "(" (Set (Var "R"))  ($#k7_lattice3 :::"~"::: )  ")" )))  ($#r1_relset_1 :::"c="::: )  (Set   ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))))) ; 
 definitionlet "L" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Const "L")) "," (Set (Const "L")) ($#k3_yellow_3 :::":]"::: ) ) "," (Set (Const "L")); let "a", "b" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); :: original: :::"."::: redefine func "f" :::".":::  "(" "a" "," "b" ")"  ->   ($#m1_subset_1 :::"Element":::) "of" "L"; end; 
theorem :: YELLOW12:24 (Bool  "for" (Set (Var "R")) "being"   ($#v2_yellow_0 :::"upper-bounded"::: )    ($#l1_orders_2 :::"Semilattice":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "R")) "," (Set (Var "R")) ($#k3_yellow_3 :::":]"::: ) )  "st" (Bool (Bool   ($#r2_yellow_0 :::"ex_inf_of"::: )  (Set (Set  "("  ($#k4_waybel_2 :::"inf_op"::: )  (Set (Var "R")) ")" )  ($#k7_relset_1 :::".:"::: )  (Set (Var "X"))) "," (Set (Var "R")))) "holds"  (Bool (Set   ($#k4_waybel_2 :::"inf_op"::: )  (Set (Var "R")))  ($#r3_waybel_0 :::"preserves_inf_of"::: )  (Set (Var "X"))))) ; 
 registrationlet "R" be   ($#v3_lattice3 :::"complete"::: )    ($#l1_orders_2 :::"Semilattice":::); 
cluster (Set   ($#k4_waybel_2 :::"inf_op"::: )  "R") ->   ($#v17_waybel_0 :::"infs-preserving"::: )   ; 
end; 
theorem :: YELLOW12:25 (Bool  "for" (Set (Var "R")) "being"   ($#v1_yellow_0 :::"lower-bounded"::: )    ($#l1_orders_2 :::"sup-Semilattice":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "R")) "," (Set (Var "R")) ($#k3_yellow_3 :::":]"::: ) )  "st" (Bool (Bool   ($#r1_yellow_0 :::"ex_sup_of"::: )  (Set (Set  "("  ($#k5_waybel_2 :::"sup_op"::: )  (Set (Var "R")) ")" )  ($#k7_relset_1 :::".:"::: )  (Set (Var "X"))) "," (Set (Var "R")))) "holds"  (Bool (Set   ($#k5_waybel_2 :::"sup_op"::: )  (Set (Var "R")))  ($#r4_waybel_0 :::"preserves_sup_of"::: )  (Set (Var "X"))))) ; 
 registrationlet "R" be   ($#v3_lattice3 :::"complete"::: )    ($#l1_orders_2 :::"sup-Semilattice":::); 
cluster (Set   ($#k5_waybel_2 :::"sup_op"::: )  "R") ->   ($#v18_waybel_0 :::"sups-preserving"::: )   ; 
end; 
theorem :: YELLOW12:26 (Bool  "for" (Set (Var "N")) "being"   ($#l1_orders_2 :::"Semilattice":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N"))  "st" (Bool (Bool (Set   ($#k5_yellow_0 :::"subrelstr"::: )  (Set (Var "A"))) "is"   ($#v5_yellow_0 :::"meet-inheriting"::: )  )) "holds"  (Bool (Set (Var "A")) "is"   ($#v2_waybel_0 :::"filtered"::: )  ))) ; 
 
theorem :: YELLOW12:27 (Bool  "for" (Set (Var "N")) "being"   ($#l1_orders_2 :::"sup-Semilattice":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N"))  "st" (Bool (Bool (Set   ($#k5_yellow_0 :::"subrelstr"::: )  (Set (Var "A"))) "is"   ($#v6_yellow_0 :::"join-inheriting"::: )  )) "holds"  (Bool (Set (Var "A")) "is"   ($#v1_waybel_0 :::"directed"::: )  ))) ; 
 
theorem :: YELLOW12:28 (Bool  "for" (Set (Var "N")) "being"   ($#v4_orders_2 :::"transitive"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "J")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N"))  "st" (Bool (Bool (Set (Var "A"))  ($#r2_yellow_4 :::"is_coarser_than"::: )  (Set   ($#k4_waybel_0 :::"uparrow"::: )  (Set (Var "J"))))) "holds"  (Bool (Set   ($#k4_waybel_0 :::"uparrow"::: )  (Set (Var "A")))  ($#r1_tarski :::"c="::: )  (Set   ($#k4_waybel_0 :::"uparrow"::: )  (Set (Var "J")))))) ; 
 
theorem :: YELLOW12:29 (Bool  "for" (Set (Var "N")) "being"   ($#v4_orders_2 :::"transitive"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "J")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_yellow_4 :::"is_finer_than"::: )  (Set   ($#k3_waybel_0 :::"downarrow"::: )  (Set (Var "J"))))) "holds"  (Bool (Set   ($#k3_waybel_0 :::"downarrow"::: )  (Set (Var "A")))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_waybel_0 :::"downarrow"::: )  (Set (Var "J")))))) ; 
 
theorem :: YELLOW12:30 (Bool  "for" (Set (Var "N")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N"))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set   ($#k6_waybel_0 :::"uparrow"::: )  (Set (Var "x")))  ($#r1_tarski :::"c="::: )  (Set   ($#k4_waybel_0 :::"uparrow"::: )  (Set (Var "X"))))))) ; 
 
theorem :: YELLOW12:31 (Bool  "for" (Set (Var "N")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N"))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set   ($#k5_waybel_0 :::"downarrow"::: )  (Set (Var "x")))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_waybel_0 :::"downarrow"::: )  (Set (Var "X"))))))) ; 
 begin  





theorem :: YELLOW12:32 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "S"))  "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"))) "#)" ))) "holds"  (Bool (Set (Var "B")) "is"   ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T"))))) ; 
 
theorem :: YELLOW12:33 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"prebasis":::) "of" (Set (Var "S"))  "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"))) "#)" ))) "holds"  (Bool (Set (Var "B")) "is"   ($#m1_subset_1 :::"prebasis":::) "of" (Set (Var "T"))))) ; 
 
theorem :: YELLOW12:34 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "J")) "being"   ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T"))  "holds" (Bool (Bool  "not" (Set (Var "J")) "is"   ($#v1_xboole_0 :::"empty"::: )  )))) ; 
 registrationlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); 
cluster   ($#v1_tops_2 :::"open"::: )     ($#v1_cantor_1 :::"quasi_basis"::: )    ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T") ")" )); 
end; 
theorem :: YELLOW12:35 (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 (Var "T"))  (Bool  "for" (Set (Var "J")) "being"   ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "x"))  "holds" (Bool (Bool  "not" (Set (Var "J")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))))) ; 
 registrationlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); let "x" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); 
cluster   ($#v1_tops_2 :::"open"::: )   bbbadV1_YELLOW_8("T" "," "x")  ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T") ")" )); 
end; 
theorem :: YELLOW12:36 (Bool  "for" (Set (Var "S1")) "," (Set (Var "T1")) "," (Set (Var "S2")) "," (Set (Var "T2")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S1")) "," (Set (Var "S2"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T1")) "," (Set (Var "T2"))  "st" (Bool (Bool (Set   ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S1"))) "," (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "S1"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T1"))) "," (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T1"))) "#)" )) & (Bool (Set   ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S2"))) "," (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "S2"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T2"))) "," (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T2"))) "#)" )) & (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "g"))) & (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  )) "holds"  (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  )))) ; 
 
theorem :: YELLOW12:37 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "T")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) ) : (Bool (Set (Set  "("  ($#k9_funct_3 :::"pr1"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k10_funct_3 :::"pr2"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "p"))))  "}"  )) ; 
 
theorem :: YELLOW12:38 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k12_funct_3 :::"delta"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T")))) "is"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "T")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) ))) ; 
 
theorem :: YELLOW12:39 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k9_funct_3 :::"pr1"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) ")" ) "is"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Var "S")))) ; 
 
theorem :: YELLOW12:40 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k10_funct_3 :::"pr2"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) ")" ) "is"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Var "T")))) ; 
 
theorem :: YELLOW12:41 (Bool  "for" (Set (Var "T")) "," (Set (Var "S")) "," (Set (Var "R")) "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 "T")) "," (Set (Var "S"))  (Bool  "for" (Set (Var "g")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "R")) "holds"  (Bool (Set  ($#k14_funct_3 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k14_funct_3 :::":>"::: ) ) "is"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "R")) ($#k2_borsuk_1 :::":]"::: ) ))))) ; 
 
theorem :: YELLOW12:42 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set  ($#k14_funct_3 :::"<:"::: ) (Set  "("  ($#k10_funct_3 :::"pr2"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) ")"  ")" ) "," (Set  "("  ($#k9_funct_3 :::"pr1"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) ")"  ")" ) ($#k14_funct_3 :::":>"::: ) ) "is"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "T")) "," (Set (Var "S")) ($#k2_borsuk_1 :::":]"::: ) ))) ; 
 
theorem :: YELLOW12:43 (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 "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "T")) "," (Set (Var "S")) ($#k2_borsuk_1 :::":]"::: ) )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_funct_2 :::"="::: )  (Set  ($#k14_funct_3 :::"<:"::: ) (Set  "("  ($#k10_funct_3 :::"pr2"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) ")"  ")" ) "," (Set  "("  ($#k9_funct_3 :::"pr1"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) ")"  ")" ) ($#k14_funct_3 :::":>"::: ) ))) "holds"  (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ))) ; 
 
theorem :: YELLOW12:44 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "T")) "," (Set (Var "S")) ($#k2_borsuk_1 :::":]"::: ) )  ($#r1_t_0topsp :::"are_homeomorphic"::: )  )) ; 
 
theorem :: YELLOW12:45 (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"::: )   )    ($#v8_pre_topc :::"Hausdorff"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds"   (Bool  "("  (Bool  "("   "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) : (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p"))))  "}"  )) "holds"  (Bool (Set (Var "X")) "is"   ($#v3_pre_topc :::"open"::: )  )  ")" ) & (Bool  "("   "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) : (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p"))))  "}"  )) "holds"  (Bool (Set (Var "X")) "is"   ($#v4_pre_topc :::"closed"::: )  )  ")" )  ")" )))) ; 
 
theorem :: YELLOW12:46 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"   (Bool  "("  (Bool (Set (Var "T")) "is"   ($#v8_pre_topc :::"Hausdorff"::: )  ) "iff" (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "T")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T")))))) "holds"  (Bool (Set (Var "A")) "is"   ($#v4_pre_topc :::"closed"::: )  ))  ")" )) ; 
 registrationlet "S", "T" be    ($#l1_pre_topc :::"TopStruct"::: )  ; 
cluster   ($#v1_pre_topc :::"strict"::: )     ($#v2_pre_topc :::"TopSpace-like"::: )    for    ($#m3_yellow_9 :::"Refinement"::: )   "of" "S" "," "T"; 
end; registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_pre_topc :::"TopStruct"::: )  ; let "T" be    ($#l1_pre_topc :::"TopStruct"::: )  ; 
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_pre_topc :::"strict"::: )     ($#v2_pre_topc :::"TopSpace-like"::: )    for    ($#m3_yellow_9 :::"Refinement"::: )   "of" "S" "," "T"; 

cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_pre_topc :::"strict"::: )     ($#v2_pre_topc :::"TopSpace-like"::: )    for    ($#m3_yellow_9 :::"Refinement"::: )   "of" "T" "," "S"; 
end; 
theorem :: YELLOW12:47 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "," (Set (Var "T")) "being"    ($#l1_pre_topc :::"TopStruct"::: )   "holds"   (Bool  "("  (Bool (Set (Var "R")) "is"    ($#m3_yellow_9 :::"Refinement"::: )   "of" (Set (Var "S")) "," (Set (Var "T"))) "iff" (Bool (Set   ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R"))) "," (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "R"))) "#)" ) "is"    ($#m3_yellow_9 :::"Refinement"::: )   "of" (Set (Var "S")) "," (Set (Var "T")))  ")" )) ; 
 















theorem :: YELLOW12:48 (Bool  "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "T1")) "," (Set (Var "T2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "R")) "being"    ($#m3_yellow_9 :::"Refinement"::: )   "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "S1")) "," (Set (Var "T1")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "S2")) "," (Set (Var "T2")) ($#k2_borsuk_1 :::":]"::: ) )  "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S1")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S2")))) & (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T1")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T2"))))) "holds"  (Bool  "{"  (Set  "(" (Set  ($#k3_borsuk_1 :::"[:"::: ) (Set (Var "U1")) "," (Set (Var "V1")) ($#k3_borsuk_1 :::":]"::: ) )  ($#k9_subset_1 :::"/\"::: )  (Set  ($#k3_borsuk_1 :::"[:"::: ) (Set (Var "U2")) "," (Set (Var "V2")) ($#k3_borsuk_1 :::":]"::: ) ) ")" ) where U1 "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S1")), U2 "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S2")), V1 "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T1")), V2 "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T2")) : (Bool  "("  (Bool (Set (Var "U1")) "is"   ($#v3_pre_topc :::"open"::: )  ) & (Bool (Set (Var "U2")) "is"   ($#v3_pre_topc :::"open"::: )  ) & (Bool (Set (Var "V1")) "is"   ($#v3_pre_topc :::"open"::: )  ) & (Bool (Set (Var "V2")) "is"   ($#v3_pre_topc :::"open"::: )  )  ")" )  "}"   "is"   ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "R"))))) ; 
 
theorem :: YELLOW12:49 (Bool  "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "T1")) "," (Set (Var "T2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "R")) "being"    ($#m3_yellow_9 :::"Refinement"::: )   "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "S1")) "," (Set (Var "T1")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "S2")) "," (Set (Var "T2")) ($#k2_borsuk_1 :::":]"::: ) )  (Bool  "for" (Set (Var "R1")) "being"    ($#m3_yellow_9 :::"Refinement"::: )   "of" (Set (Var "S1")) "," (Set (Var "S2"))  (Bool  "for" (Set (Var "R2")) "being"    ($#m3_yellow_9 :::"Refinement"::: )   "of" (Set (Var "T1")) "," (Set (Var "T2"))  "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S1")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S2")))) & (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T1")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T2"))))) "holds"  (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "R1")) "," (Set (Var "R2")) ($#k2_borsuk_1 :::":]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))) & (Bool (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "R1")) "," (Set (Var "R2")) ($#k2_borsuk_1 :::":]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "R"))))  ")" ))))) ; 
 
theorem :: YELLOW12:50 (Bool  "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "T1")) "," (Set (Var "T2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "R1")) "being"    ($#m3_yellow_9 :::"Refinement"::: )   "of" (Set (Var "S1")) "," (Set (Var "S2"))  (Bool  "for" (Set (Var "R2")) "being"    ($#m3_yellow_9 :::"Refinement"::: )   "of" (Set (Var "T1")) "," (Set (Var "T2"))  "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S1")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S2")))) & (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T1")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T2"))))) "holds"  (Bool (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "R1")) "," (Set (Var "R2")) ($#k2_borsuk_1 :::":]"::: ) ) "is"    ($#m3_yellow_9 :::"Refinement"::: )   "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "S1")) "," (Set (Var "T1")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "S2")) "," (Set (Var "T2")) ($#k2_borsuk_1 :::":]"::: ) ))))) ;