:: WAYBEL24  semantic presentation begin  
theorem :: WAYBEL24:1 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"   ($#v24_waybel_0 :::"up-complete"::: )     ($#v4_waybel11 :::"Scott"::: )    ($#l1_waybel_9 :::"TopLattice":::)  (Bool  "for" (Set (Var "M")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k2_waybel17 :::"SCMaps"::: )   "(" (Set (Var "S")) "," (Set (Var "T")) ")"  ")" ) "holds"  (Bool (Set   ($#k1_yellow_0 :::""\/""::: )   "(" (Set (Var "M")) "," (Set  "("  ($#k2_waybel17 :::"SCMaps"::: )   "(" (Set (Var "S")) "," (Set (Var "T")) ")"  ")" ) ")" ) "is"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))))) ; 
 registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; let "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; 
cluster   ($#v1_funct_1 :::"Function-like"::: )     ($#v3_funct_1 :::"constant"::: )     ($#v1_funct_2 :::"quasi_total"::: )    ->   ($#v5_orders_3 :::"monotone"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T") ($#k2_zfmisc_1 :::":]"::: ) )); 
end; registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; let "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; let "a" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "T")); 
cluster (Set "S"  ($#k6_struct_0 :::"-->"::: )  "a") ->   ($#v5_orders_3 :::"monotone"::: )   ; 
end; 
theorem :: WAYBEL24:2 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v1_yellow_0 :::"lower-bounded"::: )     ($#l1_orders_2 :::"RelStr"::: )   "holds"  (Bool (Set   ($#k3_yellow_0 :::"Bottom"::: )  (Set  "("  ($#k7_yellow_1 :::"MonMaps"::: )   "(" (Set (Var "S")) "," (Set (Var "T")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "S"))  ($#k6_struct_0 :::"-->"::: )  (Set  "("  ($#k3_yellow_0 :::"Bottom"::: )  (Set (Var "T")) ")" ))))) ; 
 
theorem :: WAYBEL24:3 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v2_yellow_0 :::"upper-bounded"::: )     ($#l1_orders_2 :::"RelStr"::: )   "holds"  (Bool (Set   ($#k4_yellow_0 :::"Top"::: )  (Set  "("  ($#k7_yellow_1 :::"MonMaps"::: )   "(" (Set (Var "S")) "," (Set (Var "T")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "S"))  ($#k6_struct_0 :::"-->"::: )  (Set  "("  ($#k4_yellow_0 :::"Top"::: )  (Set (Var "T")) ")" ))))) ; 
 scheme  :: WAYBEL24:sch 1 FuncFraenkelSL{ F1() ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  , F2() ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  , F3(   ($#m1_hidden :::"set"::: )  ) ->   ($#m1_subset_1 :::"Element":::) "of" (Set F2 "("  ")" ), F4() ->   ($#m1_hidden :::"Function":::), P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool (Set (Set F4 "("  ")" )  ($#k7_relat_1 :::".:"::: )   "{"  (Set F3 "(" (Set (Var "x")) ")" ) where x "is"   ($#m1_subset_1 :::"Element":::) "of" (Set F1 "("  ")" ) : (Bool P1[(Set (Var "x"))])  "}"  )  ($#r1_hidden :::"="::: )   "{"  (Set  "(" (Set F4 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set F3 "(" (Set (Var "x")) ")" ) ")" ) where x "is"   ($#m1_subset_1 :::"Element":::) "of" (Set F1 "("  ")" ) : (Bool P1[(Set (Var "x"))])  "}"  )
 provided
(Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set F2 "("  ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set F4 "("  ")" )))
 proof 


end; scheme  :: WAYBEL24:sch 2 Fraenkel6A{ F1() ->   ($#l1_orders_2 :::"LATTICE":::), F2(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )  ], P2[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "{"  (Set F2 "(" (Set (Var "v1")) ")" ) where v1 "is"   ($#m1_subset_1 :::"Element":::) "of" (Set F1 "("  ")" ) : (Bool P1[(Set (Var "v1"))])  "}"    ($#r1_hidden :::"="::: )   "{"  (Set F2 "(" (Set (Var "v2")) ")" ) where v2 "is"   ($#m1_subset_1 :::"Element":::) "of" (Set F1 "("  ")" ) : (Bool P2[(Set (Var "v2"))])  "}"  )
 provided
(Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set F1 "("  ")" ) "holds"   (Bool  "("  (Bool P1[(Set (Var "v"))]) "iff" (Bool P2[(Set (Var "v"))])  ")" ))
 proof 


end; 
theorem :: WAYBEL24:4 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"   ($#v3_lattice3 :::"complete"::: )    ($#l1_orders_2 :::"LATTICE":::)  (Bool  "for" (Set (Var "f")) "being"   ($#v5_orders_3 :::"monotone"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_yellow_0 :::"sup"::: )  (Set  "(" (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set  "("  ($#k5_waybel_0 :::"downarrow"::: )  (Set (Var "x")) ")" ) ")" )))))) ; 
 
theorem :: WAYBEL24:5 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"   ($#v1_yellow_0 :::"lower-bounded"::: )     ($#v3_lattice3 :::"complete"::: )    ($#l1_orders_2 :::"LATTICE":::)  (Bool  "for" (Set (Var "f")) "being"   ($#v5_orders_3 :::"monotone"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_yellow_0 :::""\/""::: )   "("  "{"  (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "w")) ")" ) where w "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) : (Bool (Set (Var "w"))  ($#r3_orders_2 :::"<="::: )  (Set (Var "x")))  "}"   "," (Set (Var "T")) ")" ))))) ; 
 
theorem :: WAYBEL24:6 (Bool  "for" (Set (Var "S")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Var "T"))  ($#k6_yellow_1 :::"|^"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) ")" ) "holds"  (Bool (Set   ($#k1_yellow_0 :::"sup"::: )  (Set (Var "F"))) "is"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")))))) ; 
 begin  definitionlet "X1", "X2", "Y" 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 "X1")) "," (Set (Const "X2")) ($#k3_yellow_3 :::":]"::: ) ) "," (Set (Const "Y")); let "x" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X1")); func  :::"Proj":::  "(" "f" "," "x" ")"  ->   ($#m1_subset_1 :::"Function":::) "of" "X2" "," "Y" equals :: WAYBEL24:def 1 (Set (Set  "("  ($#k1_funct_5 :::"curry"::: )  "f" ")" )  ($#k1_funct_1 :::"."::: )  "x"); end; 









:: deftheorem    defines :::"Proj"::: WAYBEL24:def 1 :  (Bool  "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) ($#k3_yellow_3 :::":]"::: ) ) "," (Set (Var "Y"))  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X1")) "holds"  (Bool (Set   ($#k1_waybel24 :::"Proj"::: )   "(" (Set (Var "f")) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_funct_5 :::"curry"::: )  (Set (Var "f")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x"))))))); 
 














theorem :: WAYBEL24:7 (Bool  "for" (Set (Var "Y")) "," (Set (Var "X1")) "," (Set (Var "X2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) ($#k3_yellow_3 :::":]"::: ) ) "," (Set (Var "Y"))  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X1"))  (Bool  "for" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X2")) "holds"  (Bool (Set (Set  "("  ($#k1_waybel24 :::"Proj"::: )   "(" (Set (Var "f")) "," (Set (Var "x")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))))) ; 
 definitionlet "X1", "X2", "Y" 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 "X1")) "," (Set (Const "X2")) ($#k3_yellow_3 :::":]"::: ) ) "," (Set (Const "Y")); let "y" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X2")); func  :::"Proj":::  "(" "f" "," "y" ")"  ->   ($#m1_subset_1 :::"Function":::) "of" "X1" "," "Y" equals :: WAYBEL24:def 2 (Set (Set  "("  ($#k3_funct_5 :::"curry'"::: )  "f" ")" )  ($#k1_funct_1 :::"."::: )  "y"); end; 









:: deftheorem    defines :::"Proj"::: WAYBEL24:def 2 :  (Bool  "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) ($#k3_yellow_3 :::":]"::: ) ) "," (Set (Var "Y"))  (Bool  "for" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X2")) "holds"  (Bool (Set   ($#k2_waybel24 :::"Proj"::: )   "(" (Set (Var "f")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_funct_5 :::"curry'"::: )  (Set (Var "f")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "y"))))))); 
 
theorem :: WAYBEL24:8 (Bool  "for" (Set (Var "Y")) "," (Set (Var "X2")) "," (Set (Var "X1")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) ($#k3_yellow_3 :::":]"::: ) ) "," (Set (Var "Y"))  (Bool  "for" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X2"))  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X1")) "holds"  (Bool (Set (Set  "("  ($#k2_waybel24 :::"Proj"::: )   "(" (Set (Var "f")) "," (Set (Var "y")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))))) ; 
 
theorem :: WAYBEL24:9 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "R")) "," (Set (Var "S")) ($#k3_yellow_3 :::":]"::: ) ) "," (Set (Var "T"))  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds"  (Bool (Set (Set  "("  ($#k1_waybel24 :::"Proj"::: )   "(" (Set (Var "f")) "," (Set (Var "a")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_waybel24 :::"Proj"::: )   "(" (Set (Var "f")) "," (Set (Var "b")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))))))) ; 
 registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; let "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_relat_1 :::"Relation-like"::: )   (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S")  ($#v4_relat_1 :::"-defined"::: )   (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T")  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_PARTFUN1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S"))   ($#v1_funct_2 :::"quasi_total"::: )     ($#v5_waybel_0 :::"antitone"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T") ($#k2_zfmisc_1 :::":]"::: ) )); 
end; 
theorem :: WAYBEL24:10 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "R")) "," (Set (Var "S")) ($#k3_yellow_3 :::":]"::: ) ) "," (Set (Var "T"))  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v5_orders_3 :::"monotone"::: )  )) "holds"  (Bool  "("  (Bool (Set   ($#k1_waybel24 :::"Proj"::: )   "(" (Set (Var "f")) "," (Set (Var "a")) ")" ) "is"   ($#v5_orders_3 :::"monotone"::: )  ) & (Bool (Set   ($#k2_waybel24 :::"Proj"::: )   "(" (Set (Var "f")) "," (Set (Var "b")) ")" ) "is"   ($#v5_orders_3 :::"monotone"::: )  )  ")" ))))) ; 
 
theorem :: WAYBEL24:11 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "R")) "," (Set (Var "S")) ($#k3_yellow_3 :::":]"::: ) ) "," (Set (Var "T"))  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v5_waybel_0 :::"antitone"::: )  )) "holds"  (Bool  "("  (Bool (Set   ($#k1_waybel24 :::"Proj"::: )   "(" (Set (Var "f")) "," (Set (Var "a")) ")" ) "is"   ($#v5_waybel_0 :::"antitone"::: )  ) & (Bool (Set   ($#k2_waybel24 :::"Proj"::: )   "(" (Set (Var "f")) "," (Set (Var "b")) ")" ) "is"   ($#v5_waybel_0 :::"antitone"::: )  )  ")" ))))) ; 
 registrationlet "R", "S", "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; let "f" be   ($#v5_orders_3 :::"monotone"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Const "R")) "," (Set (Const "S")) ($#k3_yellow_3 :::":]"::: ) ) "," (Set (Const "T")); let "a" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); 
cluster (Set   ($#k1_waybel24 :::"Proj"::: )   "(" "f" "," "a" ")" ) ->   ($#v5_orders_3 :::"monotone"::: )   ; 
end; registrationlet "R", "S", "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; let "f" be   ($#v5_orders_3 :::"monotone"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Const "R")) "," (Set (Const "S")) ($#k3_yellow_3 :::":]"::: ) ) "," (Set (Const "T")); let "b" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); 
cluster (Set   ($#k2_waybel24 :::"Proj"::: )   "(" "f" "," "b" ")" ) ->   ($#v5_orders_3 :::"monotone"::: )   ; 
end; registrationlet "R", "S", "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; let "f" be   ($#v5_waybel_0 :::"antitone"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Const "R")) "," (Set (Const "S")) ($#k3_yellow_3 :::":]"::: ) ) "," (Set (Const "T")); let "a" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); 
cluster (Set   ($#k1_waybel24 :::"Proj"::: )   "(" "f" "," "a" ")" ) ->   ($#v5_waybel_0 :::"antitone"::: )   ; 
end; registrationlet "R", "S", "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; let "f" be   ($#v5_waybel_0 :::"antitone"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Const "R")) "," (Set (Const "S")) ($#k3_yellow_3 :::":]"::: ) ) "," (Set (Const "T")); let "b" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); 
cluster (Set   ($#k2_waybel24 :::"Proj"::: )   "(" "f" "," "b" ")" ) ->   ($#v5_waybel_0 :::"antitone"::: )   ; 
end; 
theorem :: WAYBEL24:12 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "," (Set (Var "T")) "being"   ($#l1_orders_2 :::"LATTICE":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "R")) "," (Set (Var "S")) ($#k3_yellow_3 :::":]"::: ) ) "," (Set (Var "T"))  "st" (Bool (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds"   (Bool  "("  (Bool (Set   ($#k1_waybel24 :::"Proj"::: )   "(" (Set (Var "f")) "," (Set (Var "a")) ")" ) "is"   ($#v5_orders_3 :::"monotone"::: )  ) & (Bool (Set   ($#k2_waybel24 :::"Proj"::: )   "(" (Set (Var "f")) "," (Set (Var "b")) ")" ) "is"   ($#v5_orders_3 :::"monotone"::: )  )  ")" ))  ")" )) "holds"  (Bool (Set (Var "f")) "is"   ($#v5_orders_3 :::"monotone"::: )  ))) ; 
 
theorem :: WAYBEL24:13 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "," (Set (Var "T")) "being"   ($#l1_orders_2 :::"LATTICE":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "R")) "," (Set (Var "S")) ($#k3_yellow_3 :::":]"::: ) ) "," (Set (Var "T"))  "st" (Bool (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds"   (Bool  "("  (Bool (Set   ($#k1_waybel24 :::"Proj"::: )   "(" (Set (Var "f")) "," (Set (Var "a")) ")" ) "is"   ($#v5_waybel_0 :::"antitone"::: )  ) & (Bool (Set   ($#k2_waybel24 :::"Proj"::: )   "(" (Set (Var "f")) "," (Set (Var "b")) ")" ) "is"   ($#v5_waybel_0 :::"antitone"::: )  )  ")" ))  ")" )) "holds"  (Bool (Set (Var "f")) "is"   ($#v5_waybel_0 :::"antitone"::: )  ))) ; 
 
theorem :: WAYBEL24:14 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "," (Set (Var "T")) "being"   ($#l1_orders_2 :::"LATTICE":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "R")) "," (Set (Var "S")) ($#k3_yellow_3 :::":]"::: ) ) "," (Set (Var "T"))  (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "holds"  (Bool (Set (Set  "("  ($#k2_waybel24 :::"Proj"::: )   "(" (Set (Var "f")) "," (Set (Var "b")) ")"  ")" )  ($#k7_relset_1 :::".:"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set  ($#k6_yellow_3 :::"[:"::: ) (Set (Var "X")) "," (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "b")) ($#k6_domain_1 :::"}"::: ) ) ($#k6_yellow_3 :::":]"::: ) ))))))) ; 
 
theorem :: WAYBEL24:15 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "," (Set (Var "T")) "being"   ($#l1_orders_2 :::"LATTICE":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "R")) "," (Set (Var "S")) ($#k3_yellow_3 :::":]"::: ) ) "," (Set (Var "T"))  (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds"  (Bool (Set (Set  "("  ($#k1_waybel24 :::"Proj"::: )   "(" (Set (Var "f")) "," (Set (Var "b")) ")"  ")" )  ($#k7_relset_1 :::".:"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set  ($#k6_yellow_3 :::"[:"::: ) (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "b")) ($#k6_domain_1 :::"}"::: ) ) "," (Set (Var "X")) ($#k6_yellow_3 :::":]"::: ) ))))))) ; 
 
theorem :: WAYBEL24:16 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "," (Set (Var "T")) "being"   ($#l1_orders_2 :::"LATTICE":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "R")) "," (Set (Var "S")) ($#k3_yellow_3 :::":]"::: ) ) "," (Set (Var "T"))  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v22_waybel_0 :::"directed-sups-preserving"::: )  )) "holds"  (Bool  "("  (Bool (Set   ($#k1_waybel24 :::"Proj"::: )   "(" (Set (Var "f")) "," (Set (Var "a")) ")" ) "is"   ($#v22_waybel_0 :::"directed-sups-preserving"::: )  ) & (Bool (Set   ($#k2_waybel24 :::"Proj"::: )   "(" (Set (Var "f")) "," (Set (Var "b")) ")" ) "is"   ($#v22_waybel_0 :::"directed-sups-preserving"::: )  )  ")" ))))) ; 
 
theorem :: WAYBEL24:17 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "," (Set (Var "T")) "being"   ($#l1_orders_2 :::"LATTICE":::)  (Bool  "for" (Set (Var "f")) "being"   ($#v5_orders_3 :::"monotone"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "R")) "," (Set (Var "S")) ($#k3_yellow_3 :::":]"::: ) ) "," (Set (Var "T"))  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "X")) "being"   ($#v1_waybel_0 :::"directed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "R")) "," (Set (Var "S")) ($#k3_yellow_3 :::":]"::: ) )  "st" (Bool (Bool   ($#r1_yellow_0 :::"ex_sup_of"::: )  (Set (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "X"))) "," (Set (Var "T"))) & (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_yellow_3 :::"proj1"::: )  (Set (Var "X")))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set   ($#k5_yellow_3 :::"proj2"::: )  (Set (Var "X"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  ($#k7_yellow_3 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k7_yellow_3 :::"]"::: ) ))  ($#r3_orders_2 :::"<="::: )  (Set   ($#k1_yellow_0 :::"sup"::: )  (Set  "(" (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "X")) ")" )))))))) ; 
 
theorem :: WAYBEL24:18 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "," (Set (Var "T")) "being"   ($#v3_lattice3 :::"complete"::: )    ($#l1_orders_2 :::"LATTICE":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "R")) "," (Set (Var "S")) ($#k3_yellow_3 :::":]"::: ) ) "," (Set (Var "T"))  "st" (Bool (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds"   (Bool  "("  (Bool (Set   ($#k1_waybel24 :::"Proj"::: )   "(" (Set (Var "f")) "," (Set (Var "a")) ")" ) "is"   ($#v22_waybel_0 :::"directed-sups-preserving"::: )  ) & (Bool (Set   ($#k2_waybel24 :::"Proj"::: )   "(" (Set (Var "f")) "," (Set (Var "b")) ")" ) "is"   ($#v22_waybel_0 :::"directed-sups-preserving"::: )  )  ")" ))  ")" )) "holds"  (Bool (Set (Var "f")) "is"   ($#v22_waybel_0 :::"directed-sups-preserving"::: )  ))) ; 
 
theorem :: WAYBEL24:19 (Bool  "for" (Set (Var "S")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "f")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Var "T"))  ($#k6_yellow_1 :::"|^"::: )  (Set (Var "S")) ")" )) "iff" (Bool (Set (Var "f")) "is"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))))  ")" )))) ; 
 begin  definitionlet "S" be    ($#l1_pre_topc :::"TopStruct"::: )  ; let "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_waybel_9 :::"TopRelStr"::: )  ; func  :::"ContMaps":::  "(" "S" "," "T" ")"  ->   ($#v1_orders_2 :::"strict"::: )     ($#l1_orders_2 :::"RelStr"::: )   means :: WAYBEL24:def 3 (Bool  "("  (Bool it "is"   ($#v4_yellow_0 :::"full"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set "T"  ($#k6_yellow_1 :::"|^"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S"))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)) "iff" (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" "S" "," "T" "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "f"))) & (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  )  ")" ))  ")" )  ")" )  ")" ); end; 






:: deftheorem    defines :::"ContMaps"::: WAYBEL24:def 3 :  (Bool  "for" (Set (Var "S")) "being"    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_waybel_9 :::"TopRelStr"::: )    (Bool  "for" (Set (Var "b3")) "being"   ($#v1_orders_2 :::"strict"::: )     ($#l1_orders_2 :::"RelStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_waybel24 :::"ContMaps"::: )   "(" (Set (Var "S")) "," (Set (Var "T")) ")" )) "iff" (Bool  "("  (Bool (Set (Var "b3")) "is"   ($#v4_yellow_0 :::"full"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set (Set (Var "T"))  ($#k6_yellow_1 :::"|^"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b3")))) "iff" (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "f"))) & (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  )  ")" ))  ")" )  ")" )  ")" )  ")" )))); 
 registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); let "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_pre_topc :::"TopSpace-like"::: )     ($#l1_waybel_9 :::"TopRelStr"::: )  ; 
cluster (Set   ($#k3_waybel24 :::"ContMaps"::: )   "(" "S" "," "T" ")" ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_orders_2 :::"strict"::: )   ; 
end; registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); let "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_pre_topc :::"TopSpace-like"::: )     ($#l1_waybel_9 :::"TopRelStr"::: )  ; 
cluster (Set   ($#k3_waybel24 :::"ContMaps"::: )   "(" "S" "," "T" ")" ) ->   ($#v1_monoid_0 :::"constituted-Functions"::: )     ($#v1_orders_2 :::"strict"::: )   ; 
end; 
theorem :: WAYBEL24:20 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v3_orders_2 :::"reflexive"::: )     ($#l1_waybel_9 :::"TopRelStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k3_waybel24 :::"ContMaps"::: )   "(" (Set (Var "S")) "," (Set (Var "T")) ")"  ")" ) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "y"))) "iff" (Bool  "for" (Set (Var "i")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set (Var "x"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")) ")" ) "," (Set  "(" (Set (Var "y"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")) ")" ) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "T")))))  ")" )))) ; 
 
theorem :: WAYBEL24:21 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v3_orders_2 :::"reflexive"::: )     ($#l1_waybel_9 :::"TopRelStr"::: )    (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x")) "is"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))) "iff" (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k3_waybel24 :::"ContMaps"::: )   "(" (Set (Var "S")) "," (Set (Var "T")) ")"  ")" ))  ")" )))) ; 
 registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); let "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v3_orders_2 :::"reflexive"::: )     ($#l1_waybel_9 :::"TopRelStr"::: )  ; 
cluster (Set   ($#k3_waybel24 :::"ContMaps"::: )   "(" "S" "," "T" ")" ) ->   ($#v1_orders_2 :::"strict"::: )     ($#v3_orders_2 :::"reflexive"::: )   ; 
end; registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); let "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v4_orders_2 :::"transitive"::: )     ($#l1_waybel_9 :::"TopRelStr"::: )  ; 
cluster (Set   ($#k3_waybel24 :::"ContMaps"::: )   "(" "S" "," "T" ")" ) ->   ($#v1_orders_2 :::"strict"::: )     ($#v4_orders_2 :::"transitive"::: )   ; 
end; registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); let "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#l1_waybel_9 :::"TopRelStr"::: )  ; 
cluster (Set   ($#k3_waybel24 :::"ContMaps"::: )   "(" "S" "," "T" ")" ) ->   ($#v1_orders_2 :::"strict"::: )     ($#v5_orders_2 :::"antisymmetric"::: )   ; 
end; registrationlet "S" be    ($#m1_hidden :::"set"::: )  ; let "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; 
cluster (Set "T"  ($#k6_yellow_1 :::"|^"::: )  "S") ->   ($#v1_monoid_0 :::"constituted-Functions"::: )   ; 
end; 
theorem :: WAYBEL24:22 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#v3_lattice3 :::"complete"::: )    ($#l1_orders_2 :::"LATTICE":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))  (Bool  "for" (Set (Var "i")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "h"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_yellow_0 :::""\/""::: )   "(" (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k7_domain_1 :::"}"::: ) ) "," (Set  "(" (Set (Var "T"))  ($#k6_yellow_1 :::"|^"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) ")" ) ")" ))) "holds"  (Bool (Set (Set (Var "h"))  ($#k3_funct_2 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_yellow_0 :::"sup"::: )  (Set  ($#k7_domain_1 :::"{"::: ) (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "i")) ")" ) "," (Set  "(" (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "i")) ")" ) ($#k7_domain_1 :::"}"::: ) ))))))) ; 
 
theorem :: WAYBEL24:23 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "being"   ($#v1_yellow_1 :::"RelStr-yielding"::: )     ($#v4_waybel_3 :::"non-Empty"::: )     ($#v5_waybel_3 :::"reflexive-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I")) "holds"  (Bool (Set (Set (Var "J"))  ($#k3_waybel_3 :::"."::: )  (Set (Var "i"))) "is"   ($#v3_lattice3 :::"complete"::: )    ($#l1_orders_2 :::"LATTICE":::))  ")" )) "holds"  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_yellow_1 :::"product"::: )  (Set (Var "J")) ")" )  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I")) "holds"  (Bool (Set (Set  "("  ($#k2_yellow_0 :::"inf"::: )  (Set (Var "X")) ")" )  ($#k4_waybel_3 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_yellow_0 :::"inf"::: )  (Set  "("  ($#k5_waybel_3 :::"pi"::: )   "(" (Set (Var "X")) "," (Set (Var "i")) ")"  ")" ))))))) ; 
 
theorem :: WAYBEL24:24 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#v3_lattice3 :::"complete"::: )    ($#l1_orders_2 :::"LATTICE":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))  (Bool  "for" (Set (Var "i")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "h"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_yellow_0 :::""/\""::: )   "(" (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k7_domain_1 :::"}"::: ) ) "," (Set  "(" (Set (Var "T"))  ($#k6_yellow_1 :::"|^"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) ")" ) ")" ))) "holds"  (Bool (Set (Set (Var "h"))  ($#k3_funct_2 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_yellow_0 :::"inf"::: )  (Set  ($#k7_domain_1 :::"{"::: ) (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "i")) ")" ) "," (Set  "(" (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "i")) ")" ) ($#k7_domain_1 :::"}"::: ) ))))))) ; 
 
theorem :: WAYBEL24:25 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#v3_lattice3 :::"complete"::: )    ($#l1_orders_2 :::"LATTICE":::)  (Bool  "for" (Set (Var "F")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Var "T"))  ($#k6_yellow_1 :::"|^"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) ")" )  (Bool  "for" (Set (Var "i")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds"  (Bool (Set (Set  "("  ($#k1_yellow_0 :::"sup"::: )  (Set (Var "F")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_yellow_0 :::""\/""::: )   "("  "{"  (Set  "(" (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")) ")" ) where f "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Var "T"))  ($#k6_yellow_1 :::"|^"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) ")" ) : (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set (Var "F")))  "}"   "," (Set (Var "T")) ")" )))))) ; 
 
theorem :: WAYBEL24:26 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"   ($#v3_lattice3 :::"complete"::: )    ($#l1_waybel_9 :::"TopLattice":::)  (Bool  "for" (Set (Var "F")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_waybel24 :::"ContMaps"::: )   "(" (Set (Var "S")) "," (Set (Var "T")) ")"  ")" )  (Bool  "for" (Set (Var "i")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds"  (Bool (Set (Set  "("  ($#k1_yellow_0 :::""\/""::: )   "(" (Set (Var "F")) "," (Set  "(" (Set (Var "T"))  ($#k6_yellow_1 :::"|^"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) ")" ) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_yellow_0 :::""\/""::: )   "("  "{"  (Set  "(" (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")) ")" ) where f "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Var "T"))  ($#k6_yellow_1 :::"|^"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) ")" ) : (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set (Var "F")))  "}"   "," (Set (Var "T")) ")" ))))) ; 
 






theorem :: WAYBEL24:27 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#v3_lattice3 :::"complete"::: )    ($#l1_orders_2 :::"LATTICE":::)  (Bool  "for" (Set (Var "F")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Var "T"))  ($#k6_yellow_1 :::"|^"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) ")" )  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds"  (Bool (Set (Set  "("  ($#k1_yellow_0 :::"sup"::: )  (Set (Var "F")) ")" )  ($#k7_relat_1 :::".:"::: )  (Set (Var "D")))  ($#r1_hidden :::"="::: )   "{"  (Set  "("  ($#k1_yellow_0 :::""\/""::: )   "("  "{"  (Set  "(" (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")) ")" ) where f "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Var "T"))  ($#k6_yellow_1 :::"|^"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) ")" ) : (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set (Var "F")))  "}"   "," (Set (Var "T")) ")"  ")" ) where i "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) : (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set (Var "D")))  "}"  ))))) ; 
 
theorem :: WAYBEL24:28 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"   ($#v3_lattice3 :::"complete"::: )     ($#v4_waybel11 :::"Scott"::: )    ($#l1_waybel_9 :::"TopLattice":::)  (Bool  "for" (Set (Var "F")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_waybel24 :::"ContMaps"::: )   "(" (Set (Var "S")) "," (Set (Var "T")) ")"  ")" )  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds"  (Bool (Set (Set  "("  ($#k1_yellow_0 :::""\/""::: )   "(" (Set (Var "F")) "," (Set  "(" (Set (Var "T"))  ($#k6_yellow_1 :::"|^"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) ")" ) ")"  ")" )  ($#k7_relat_1 :::".:"::: )  (Set (Var "D")))  ($#r1_hidden :::"="::: )   "{"  (Set  "("  ($#k1_yellow_0 :::""\/""::: )   "("  "{"  (Set  "(" (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")) ")" ) where f "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Var "T"))  ($#k6_yellow_1 :::"|^"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) ")" ) : (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set (Var "F")))  "}"   "," (Set (Var "T")) ")"  ")" ) where i "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) : (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set (Var "D")))  "}"  )))) ; 
 scheme  :: WAYBEL24:sch 3 FraenkelF9RS{ F1() ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_waybel_9 :::"TopRelStr"::: )  , F2(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , F3(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "{"  (Set F2 "(" (Set (Var "v1")) ")" ) where v1 "is"   ($#m1_subset_1 :::"Element":::) "of" (Set F1 "("  ")" ) : (Bool P1[(Set (Var "v1"))])  "}"    ($#r1_hidden :::"="::: )   "{"  (Set F3 "(" (Set (Var "v2")) ")" ) where v2 "is"   ($#m1_subset_1 :::"Element":::) "of" (Set F1 "("  ")" ) : (Bool P1[(Set (Var "v2"))])  "}"  )
 provided
(Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set F1 "("  ")" )  "st" (Bool (Bool P1[(Set (Var "v"))])) "holds"  (Bool (Set F2 "(" (Set (Var "v")) ")" )  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "v")) ")" )))
 proof 


end; scheme  :: WAYBEL24:sch 4 FraenkelF9RSS{ F1() ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  , F2(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , F3(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "{"  (Set F2 "(" (Set (Var "v1")) ")" ) where v1 "is"   ($#m1_subset_1 :::"Element":::) "of" (Set F1 "("  ")" ) : (Bool P1[(Set (Var "v1"))])  "}"    ($#r1_hidden :::"="::: )   "{"  (Set F3 "(" (Set (Var "v2")) ")" ) where v2 "is"   ($#m1_subset_1 :::"Element":::) "of" (Set F1 "("  ")" ) : (Bool P1[(Set (Var "v2"))])  "}"  )
 provided
(Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set F1 "("  ")" )  "st" (Bool (Bool P1[(Set (Var "v"))])) "holds"  (Bool (Set F2 "(" (Set (Var "v")) ")" )  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "v")) ")" )))
 proof 


end; scheme  :: WAYBEL24:sch 5 FuncFraenkelS{ F1() ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_waybel_9 :::"TopRelStr"::: )  , F2() ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_waybel_9 :::"TopRelStr"::: )  , F3(   ($#m1_hidden :::"set"::: )  ) ->   ($#m1_subset_1 :::"Element":::) "of" (Set F2 "("  ")" ), F4() ->   ($#m1_hidden :::"Function":::), P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool (Set (Set F4 "("  ")" )  ($#k7_relat_1 :::".:"::: )   "{"  (Set F3 "(" (Set (Var "x")) ")" ) where x "is"   ($#m1_subset_1 :::"Element":::) "of" (Set F1 "("  ")" ) : (Bool P1[(Set (Var "x"))])  "}"  )  ($#r1_hidden :::"="::: )   "{"  (Set  "(" (Set F4 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set F3 "(" (Set (Var "x")) ")" ) ")" ) where x "is"   ($#m1_subset_1 :::"Element":::) "of" (Set F1 "("  ")" ) : (Bool P1[(Set (Var "x"))])  "}"  )
 provided
(Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set F2 "("  ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set F4 "("  ")" )))
 proof 


end; 
theorem :: WAYBEL24:29 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"   ($#v3_lattice3 :::"complete"::: )     ($#v4_waybel11 :::"Scott"::: )    ($#l1_waybel_9 :::"TopLattice":::)  (Bool  "for" (Set (Var "F")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_waybel24 :::"ContMaps"::: )   "(" (Set (Var "S")) "," (Set (Var "T")) ")"  ")" ) "holds"  (Bool (Set   ($#k1_yellow_0 :::""\/""::: )   "(" (Set (Var "F")) "," (Set  "(" (Set (Var "T"))  ($#k6_yellow_1 :::"|^"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) ")" ) ")" ) "is"   ($#v5_orders_3 :::"monotone"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))))) ; 
 
theorem :: WAYBEL24:30 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"   ($#v3_lattice3 :::"complete"::: )     ($#v4_waybel11 :::"Scott"::: )    ($#l1_waybel_9 :::"TopLattice":::)  (Bool  "for" (Set (Var "F")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_waybel24 :::"ContMaps"::: )   "(" (Set (Var "S")) "," (Set (Var "T")) ")"  ")" )  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_waybel_0 :::"directed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds"  (Bool (Set   ($#k1_yellow_0 :::""\/""::: )   "("  "{"  (Set  "("  ($#k1_yellow_0 :::""\/""::: )   "("  "{"  (Set  "(" (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")) ")" ) where i "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) : (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set (Var "D")))  "}"   "," (Set (Var "T")) ")"  ")" ) where g "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Var "T"))  ($#k6_yellow_1 :::"|^"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) ")" ) : (Bool (Set (Var "g"))  ($#r2_hidden :::"in"::: )  (Set (Var "F")))  "}"   "," (Set (Var "T")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_yellow_0 :::""\/""::: )   "("  "{"  (Set  "("  ($#k1_yellow_0 :::""\/""::: )   "("  "{"  (Set  "(" (Set (Var "g9"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i9")) ")" ) where g9 "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Var "T"))  ($#k6_yellow_1 :::"|^"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) ")" ) : (Bool (Set (Var "g9"))  ($#r2_hidden :::"in"::: )  (Set (Var "F")))  "}"   "," (Set (Var "T")) ")"  ")" ) where i9 "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) : (Bool (Set (Var "i9"))  ($#r2_hidden :::"in"::: )  (Set (Var "D")))  "}"   "," (Set (Var "T")) ")" ))))) ; 
 
theorem :: WAYBEL24:31 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"   ($#v3_lattice3 :::"complete"::: )     ($#v4_waybel11 :::"Scott"::: )    ($#l1_waybel_9 :::"TopLattice":::)  (Bool  "for" (Set (Var "F")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_waybel24 :::"ContMaps"::: )   "(" (Set (Var "S")) "," (Set (Var "T")) ")"  ")" )  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_waybel_0 :::"directed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds"  (Bool (Set   ($#k1_yellow_0 :::""\/""::: )   "(" (Set  "(" (Set  "("  ($#k1_yellow_0 :::""\/""::: )   "(" (Set (Var "F")) "," (Set  "(" (Set (Var "T"))  ($#k6_yellow_1 :::"|^"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) ")" ) ")"  ")" )  ($#k7_relat_1 :::".:"::: )  (Set (Var "D")) ")" ) "," (Set (Var "T")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_yellow_0 :::""\/""::: )   "(" (Set (Var "F")) "," (Set  "(" (Set (Var "T"))  ($#k6_yellow_1 :::"|^"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) ")" ) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_yellow_0 :::"sup"::: )  (Set (Var "D")) ")" )))))) ; 
 
theorem :: WAYBEL24:32 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"   ($#v3_lattice3 :::"complete"::: )     ($#v4_waybel11 :::"Scott"::: )    ($#l1_waybel_9 :::"TopLattice":::)  (Bool  "for" (Set (Var "F")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_waybel24 :::"ContMaps"::: )   "(" (Set (Var "S")) "," (Set (Var "T")) ")"  ")" ) "holds"  (Bool (Set   ($#k1_yellow_0 :::""\/""::: )   "(" (Set (Var "F")) "," (Set  "(" (Set (Var "T"))  ($#k6_yellow_1 :::"|^"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) ")" ) ")" )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k3_waybel24 :::"ContMaps"::: )   "(" (Set (Var "S")) "," (Set (Var "T")) ")"  ")" ))))) ; 
 
theorem :: WAYBEL24:33 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v5_orders_2 :::"antisymmetric"::: )     ($#v1_yellow_0 :::"lower-bounded"::: )     ($#l1_orders_2 :::"RelStr"::: )   "holds"  (Bool (Set   ($#k3_yellow_0 :::"Bottom"::: )  (Set  "(" (Set (Var "T"))  ($#k6_yellow_1 :::"|^"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "S"))  ($#k6_struct_0 :::"-->"::: )  (Set  "("  ($#k3_yellow_0 :::"Bottom"::: )  (Set (Var "T")) ")" ))))) ; 
 
theorem :: WAYBEL24:34 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v5_orders_2 :::"antisymmetric"::: )     ($#v2_yellow_0 :::"upper-bounded"::: )     ($#l1_orders_2 :::"RelStr"::: )   "holds"  (Bool (Set   ($#k4_yellow_0 :::"Top"::: )  (Set  "(" (Set (Var "T"))  ($#k6_yellow_1 :::"|^"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "S"))  ($#k6_struct_0 :::"-->"::: )  (Set  "("  ($#k4_yellow_0 :::"Top"::: )  (Set (Var "T")) ")" ))))) ; 
 registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; let "T" be   ($#v3_lattice3 :::"complete"::: )    ($#l1_orders_2 :::"LATTICE":::); let "a" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "T")); 
cluster (Set "S"  ($#k6_struct_0 :::"-->"::: )  "a") ->   ($#v22_waybel_0 :::"directed-sups-preserving"::: )   ; 
end; 
theorem :: WAYBEL24:35 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"   ($#v3_lattice3 :::"complete"::: )     ($#v4_waybel11 :::"Scott"::: )    ($#l1_waybel_9 :::"TopLattice":::) "holds"  (Bool (Set   ($#k3_waybel24 :::"ContMaps"::: )   "(" (Set (Var "S")) "," (Set (Var "T")) ")" ) "is"   ($#v8_yellow_0 :::"sups-inheriting"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set (Set (Var "T"))  ($#k6_yellow_1 :::"|^"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))))) ; 
 registrationlet "S", "T" be   ($#v3_lattice3 :::"complete"::: )     ($#v4_waybel11 :::"Scott"::: )    ($#l1_waybel_9 :::"TopLattice":::); 
cluster (Set   ($#k3_waybel24 :::"ContMaps"::: )   "(" "S" "," "T" ")" ) ->   ($#v1_orders_2 :::"strict"::: )     ($#v3_lattice3 :::"complete"::: )   ; 
end; 
theorem :: WAYBEL24:36 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_lattice3 :::"complete"::: )     ($#v4_waybel11 :::"Scott"::: )    ($#l1_waybel_9 :::"TopLattice":::) "holds"  (Bool (Set   ($#k3_yellow_0 :::"Bottom"::: )  (Set  "("  ($#k3_waybel24 :::"ContMaps"::: )   "(" (Set (Var "S")) "," (Set (Var "T")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "S"))  ($#k6_struct_0 :::"-->"::: )  (Set  "("  ($#k3_yellow_0 :::"Bottom"::: )  (Set (Var "T")) ")" )))) ; 
 
theorem :: WAYBEL24:37 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_lattice3 :::"complete"::: )     ($#v4_waybel11 :::"Scott"::: )    ($#l1_waybel_9 :::"TopLattice":::) "holds"  (Bool (Set   ($#k4_yellow_0 :::"Top"::: )  (Set  "("  ($#k3_waybel24 :::"ContMaps"::: )   "(" (Set (Var "S")) "," (Set (Var "T")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "S"))  ($#k6_struct_0 :::"-->"::: )  (Set  "("  ($#k4_yellow_0 :::"Top"::: )  (Set (Var "T")) ")" )))) ; 
 
theorem :: WAYBEL24:38 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"   ($#v3_lattice3 :::"complete"::: )     ($#v4_waybel11 :::"Scott"::: )    ($#l1_waybel_9 :::"TopLattice":::) "holds"  (Bool (Set   ($#k2_waybel17 :::"SCMaps"::: )   "(" (Set (Var "S")) "," (Set (Var "T")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_waybel24 :::"ContMaps"::: )   "(" (Set (Var "S")) "," (Set (Var "T")) ")" ))) ;