:: YELLOW_1  semantic presentation begin  


registrationlet "L" be   ($#l3_lattices :::"Lattice":::); 
cluster (Set   ($#k3_lattice3 :::"LattPOSet"::: )  "L") ->   ($#v1_lattice3 :::"with_suprema"::: )     ($#v2_lattice3 :::"with_infima"::: )   ; 
end; registrationlet "L" be   ($#v14_lattices :::"upper-bounded"::: )    ($#l3_lattices :::"Lattice":::); 
cluster (Set   ($#k3_lattice3 :::"LattPOSet"::: )  "L") ->   ($#v2_yellow_0 :::"upper-bounded"::: )   ; 
end; registrationlet "L" be   ($#v13_lattices :::"lower-bounded"::: )    ($#l3_lattices :::"Lattice":::); 
cluster (Set   ($#k3_lattice3 :::"LattPOSet"::: )  "L") ->   ($#v1_yellow_0 :::"lower-bounded"::: )   ; 
end; registrationlet "L" be   ($#v4_lattice3 :::"complete"::: )    ($#l3_lattices :::"Lattice":::); 
cluster (Set   ($#k3_lattice3 :::"LattPOSet"::: )  "L") ->   ($#v3_lattice3 :::"complete"::: )   ; 
end; definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; :: original: :::"RelIncl"::: redefine func  :::"RelIncl"::: "X" ->   ($#m1_subset_1 :::"Order":::) "of" "X"; end; definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; func  :::"InclPoset"::: "X" ->   ($#v1_orders_2 :::"strict"::: )     ($#l1_orders_2 :::"RelStr"::: )   equals :: YELLOW_1:def 1 (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  "X" "," (Set  "("  ($#k1_yellow_1 :::"RelIncl"::: )  "X" ")" ) "#)" ); end; 





:: deftheorem    defines :::"InclPoset"::: YELLOW_1:def 1 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k2_yellow_1 :::"InclPoset"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set (Var "X")) "," (Set  "("  ($#k1_yellow_1 :::"RelIncl"::: )  (Set (Var "X")) ")" ) "#)" ))); 
 registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k2_yellow_1 :::"InclPoset"::: )  "X") ->   ($#v1_orders_2 :::"strict"::: )     ($#v3_orders_2 :::"reflexive"::: )     ($#v4_orders_2 :::"transitive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )   ; 
end; registrationlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k2_yellow_1 :::"InclPoset"::: )  "X") ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_orders_2 :::"strict"::: )   ; 
end; 
theorem :: YELLOW_1:1 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k2_yellow_1 :::"InclPoset"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "X"))) & (Bool (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set  "("  ($#k2_yellow_1 :::"InclPoset"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_yellow_1 :::"RelIncl"::: )  (Set (Var "X"))))  ")" )) ; 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; func  :::"BoolePoset"::: "X" ->   ($#v1_orders_2 :::"strict"::: )     ($#l1_orders_2 :::"RelStr"::: )   equals :: YELLOW_1:def 2 (Set   ($#k3_lattice3 :::"LattPOSet"::: )  (Set  "("  ($#k1_lattice3 :::"BooleLatt"::: )  "X" ")" )); end; 





:: deftheorem    defines :::"BoolePoset"::: YELLOW_1:def 2 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k3_yellow_1 :::"BoolePoset"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_lattice3 :::"LattPOSet"::: )  (Set  "("  ($#k1_lattice3 :::"BooleLatt"::: )  (Set (Var "X")) ")" )))); 
 registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k3_yellow_1 :::"BoolePoset"::: )  "X") ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_orders_2 :::"strict"::: )     ($#v3_orders_2 :::"reflexive"::: )     ($#v4_orders_2 :::"transitive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )   ; 
end; registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k3_yellow_1 :::"BoolePoset"::: )  "X") ->   ($#v1_orders_2 :::"strict"::: )     ($#v3_lattice3 :::"complete"::: )   ; 
end; 
theorem :: YELLOW_1:2 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k3_yellow_1 :::"BoolePoset"::: )  (Set (Var "X")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r3_orders_2 :::"<="::: )  (Set (Var "y"))) "iff" (Bool (Set (Var "x"))  ($#r1_tarski :::"c="::: )  (Set (Var "y")))  ")" ))) ; 
 
theorem :: YELLOW_1:3 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k2_yellow_1 :::"InclPoset"::: )  (Set (Var "X")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r3_orders_2 :::"<="::: )  (Set (Var "y"))) "iff" (Bool (Set (Var "x"))  ($#r1_tarski :::"c="::: )  (Set (Var "y")))  ")" ))) ; 
 
theorem :: YELLOW_1:4 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k3_yellow_1 :::"BoolePoset"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_yellow_1 :::"InclPoset"::: )  (Set  "("  ($#k9_setfam_1 :::"bool"::: )  (Set (Var "X")) ")" )))) ; 
 
theorem :: YELLOW_1:5 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k2_yellow_1 :::"InclPoset"::: )  (Set (Var "Y"))) "is"   ($#v4_yellow_0 :::"full"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set   ($#k3_yellow_1 :::"BoolePoset"::: )  (Set (Var "X")))))) ; 
 
theorem :: YELLOW_1:6 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k2_yellow_1 :::"InclPoset"::: )  (Set (Var "X"))) "is"   ($#v1_lattice3 :::"with_suprema"::: )  )) "holds"  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k2_yellow_1 :::"InclPoset"::: )  (Set (Var "X")) ")" ) "holds"  (Bool (Set (Set (Var "x"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "y")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "x"))  ($#k10_lattice3 :::""\/""::: )  (Set (Var "y")))))) ; 
 
theorem :: YELLOW_1:7 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k2_yellow_1 :::"InclPoset"::: )  (Set (Var "X"))) "is"   ($#v2_lattice3 :::"with_infima"::: )  )) "holds"  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k2_yellow_1 :::"InclPoset"::: )  (Set (Var "X")) ")" ) "holds"  (Bool (Set (Set (Var "x"))  ($#k11_lattice3 :::""/\""::: )  (Set (Var "y")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "x"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "y")))))) ; 
 
theorem :: YELLOW_1:8 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k2_yellow_1 :::"InclPoset"::: )  (Set (Var "X")) ")" )  "st" (Bool (Bool (Set (Set (Var "x"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "y")))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k10_lattice3 :::""\/""::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "y")))))) ; 
 
theorem :: YELLOW_1:9 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k2_yellow_1 :::"InclPoset"::: )  (Set (Var "X")) ")" )  "st" (Bool (Bool (Set (Set (Var "x"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "y")))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k11_lattice3 :::""/\""::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "y")))))) ; 
 
theorem :: YELLOW_1:10 (Bool  "for" (Set (Var "L")) "being"    ($#l1_orders_2 :::"RelStr"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "y"))) "iff" (Bool (Set (Var "x"))  ($#r1_tarski :::"c="::: )  (Set (Var "y")))  ")" )  ")" )) "holds"  (Bool (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "L")))  ($#r2_relset_1 :::"="::: )  (Set   ($#k1_yellow_1 :::"RelIncl"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))))) ; 
 
theorem :: YELLOW_1:11 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "y")))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  ")" )) "holds"  (Bool (Set   ($#k2_yellow_1 :::"InclPoset"::: )  (Set (Var "X"))) "is"   ($#v1_lattice3 :::"with_suprema"::: )  )) ; 
 
theorem :: YELLOW_1:12 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "y")))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  ")" )) "holds"  (Bool (Set   ($#k2_yellow_1 :::"InclPoset"::: )  (Set (Var "X"))) "is"   ($#v2_lattice3 :::"with_infima"::: )  )) ; 
 
theorem :: YELLOW_1:13 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set   ($#k3_yellow_0 :::"Bottom"::: )  (Set  "("  ($#k2_yellow_1 :::"InclPoset"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: YELLOW_1:14 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k3_tarski :::"union"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set   ($#k4_yellow_0 :::"Top"::: )  (Set  "("  ($#k2_yellow_1 :::"InclPoset"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "X"))))) ; 
 
theorem :: YELLOW_1:15 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k2_yellow_1 :::"InclPoset"::: )  (Set (Var "X"))) "is"   ($#v2_yellow_0 :::"upper-bounded"::: )  )) "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) ; 
 
theorem :: YELLOW_1:16 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k2_yellow_1 :::"InclPoset"::: )  (Set (Var "X"))) "is"   ($#v1_yellow_0 :::"lower-bounded"::: )  )) "holds"  (Bool (Set   ($#k1_setfam_1 :::"meet"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) ; 
 
theorem :: YELLOW_1:17 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k3_yellow_1 :::"BoolePoset"::: )  (Set (Var "X")) ")" ) "holds"   (Bool  "("  (Bool (Set (Set (Var "x"))  ($#k13_lattice3 :::""\/""::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "y")))) & (Bool (Set (Set (Var "x"))  ($#k12_lattice3 :::""/\""::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "y"))))  ")" ))) ; 
 
theorem :: YELLOW_1:18 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k3_yellow_0 :::"Bottom"::: )  (Set  "("  ($#k3_yellow_1 :::"BoolePoset"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: YELLOW_1:19 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k4_yellow_0 :::"Top"::: )  (Set  "("  ($#k3_yellow_1 :::"BoolePoset"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "X")))) ; 
 
theorem :: YELLOW_1:20 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_yellow_1 :::"BoolePoset"::: )  (Set (Var "X")) ")" ) "holds"  (Bool (Set   ($#k2_yellow_0 :::"inf"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_setfam_1 :::"meet"::: )  (Set (Var "Y")))))) ; 
 
theorem :: YELLOW_1:21 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_yellow_1 :::"BoolePoset"::: )  (Set (Var "X")) ")" ) "holds"  (Bool (Set   ($#k1_yellow_0 :::"sup"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "Y")))))) ; 
 
theorem :: YELLOW_1:22 (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 :::"Subset":::) "of" (Set  "("  ($#k2_yellow_1 :::"InclPoset"::: )  (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T"))) ")" ) "holds"  (Bool (Set   ($#k1_yellow_0 :::"sup"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "X")))))) ; 
 
theorem :: YELLOW_1:23 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k3_yellow_0 :::"Bottom"::: )  (Set  "("  ($#k2_yellow_1 :::"InclPoset"::: )  (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T"))) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: YELLOW_1:24 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k4_yellow_0 :::"Top"::: )  (Set  "("  ($#k2_yellow_1 :::"InclPoset"::: )  (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T"))) ")" ))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))))) ; 
 registrationlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); 
cluster (Set   ($#k2_yellow_1 :::"InclPoset"::: )  (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" "T")) ->  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )    ($#v1_orders_2 :::"strict"::: )     ($#v3_lattice3 :::"complete"::: )   ; 
end; 
theorem :: YELLOW_1:25 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds"   (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v1_tops_2 :::"open"::: )  ) "iff" (Bool (Set (Var "F")) "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k2_yellow_1 :::"InclPoset"::: )  (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T"))) ")" ))  ")" ))) ; 
 begin  




definitionlet "R" be   ($#m1_hidden :::"Relation":::); attr "R" is  :::"RelStr-yielding":::  means :: YELLOW_1:def 3 (Bool  "for" (Set (Var "v")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "v"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  "R"))) "holds"  (Bool (Set (Var "v")) "is"    ($#l1_orders_2 :::"RelStr"::: )  )); end; 




:: deftheorem    defines :::"RelStr-yielding"::: YELLOW_1:def 3 :  (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "holds"   (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v1_yellow_1 :::"RelStr-yielding"::: )  ) "iff" (Bool  "for" (Set (Var "v")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "v"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "R"))))) "holds"  (Bool (Set (Var "v")) "is"    ($#l1_orders_2 :::"RelStr"::: )  ))  ")" )); 
 registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_yellow_1 :::"RelStr-yielding"::: )    ->   ($#v2_pralg_1 :::"1-sorted-yielding"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "I" be    ($#m1_hidden :::"set"::: )  ; 
cluster   ($#v1_relat_1 :::"Relation-like"::: )   "I"  ($#v4_relat_1 :::"-defined"::: )     ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_PARTFUN1("I")   ($#v1_yellow_1 :::"RelStr-yielding"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; definitionlet "J" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "A" be   ($#v1_yellow_1 :::"RelStr-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "J")); let "j" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "J")); :: original: :::"."::: redefine func "A" :::"."::: "j" ->    ($#l1_orders_2 :::"RelStr"::: )  ; end; definitionlet "I" be    ($#m1_hidden :::"set"::: )  ; let "J" be   ($#v1_yellow_1 :::"RelStr-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); func  :::"product"::: "J" ->   ($#v1_orders_2 :::"strict"::: )     ($#l1_orders_2 :::"RelStr"::: )   means :: YELLOW_1:def 4 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set   ($#k4_card_3 :::"product"::: )  (Set  "("  ($#k12_pralg_1 :::"Carrier"::: )  "J" ")" ))) & (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" it  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_card_3 :::"product"::: )  (Set  "("  ($#k12_pralg_1 :::"Carrier"::: )  "J" ")" )))) "holds"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "y"))) "iff" (Bool  "ex" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::) "st"  (Bool  "("  (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "x"))) & (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set (Var "y"))) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  "I")) "holds"  (Bool  "ex" (Set (Var "R")) "being"    ($#l1_orders_2 :::"RelStr"::: )  (Bool  "ex" (Set (Var "xi")) "," (Set (Var "yi")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st"  (Bool  "("  (Bool (Set (Var "R"))  ($#r1_hidden :::"="::: )  (Set "J"  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))) & (Bool (Set (Var "xi"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))) & (Bool (Set (Var "yi"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))) & (Bool (Set (Var "xi"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "yi")))  ")" )))  ")" )  ")" ))  ")" )  ")" )  ")" ); end; 






:: deftheorem    defines :::"product"::: YELLOW_1:def 4 :  (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "being"   ($#v1_yellow_1 :::"RelStr-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "b3")) "being"   ($#v1_orders_2 :::"strict"::: )     ($#l1_orders_2 :::"RelStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_yellow_1 :::"product"::: )  (Set (Var "J")))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_card_3 :::"product"::: )  (Set  "("  ($#k12_pralg_1 :::"Carrier"::: )  (Set (Var "J")) ")" ))) & (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "b3"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_card_3 :::"product"::: )  (Set  "("  ($#k12_pralg_1 :::"Carrier"::: )  (Set (Var "J")) ")" )))) "holds"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "y"))) "iff" (Bool  "ex" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::) "st"  (Bool  "("  (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "x"))) & (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set (Var "y"))) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set (Var "I")))) "holds"  (Bool  "ex" (Set (Var "R")) "being"    ($#l1_orders_2 :::"RelStr"::: )  (Bool  "ex" (Set (Var "xi")) "," (Set (Var "yi")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st"  (Bool  "("  (Bool (Set (Var "R"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "J"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))) & (Bool (Set (Var "xi"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))) & (Bool (Set (Var "yi"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))) & (Bool (Set (Var "xi"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "yi")))  ")" )))  ")" )  ")" ))  ")" )  ")" )  ")" )  ")" )))); 
 registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; let "L" be    ($#l1_orders_2 :::"RelStr"::: )  ; 
cluster (Set "X"  ($#k2_funcop_1 :::"-->"::: )  "L") ->   ($#v1_yellow_1 :::"RelStr-yielding"::: )   ; 
end; definitionlet "I" be    ($#m1_hidden :::"set"::: )  ; let "T" be    ($#l1_orders_2 :::"RelStr"::: )  ; func "T" :::"|^"::: "I" ->   ($#v1_orders_2 :::"strict"::: )     ($#l1_orders_2 :::"RelStr"::: )   equals :: YELLOW_1:def 5 (Set   ($#k5_yellow_1 :::"product"::: )  (Set  "(" "I"  ($#k7_funcop_1 :::"-->"::: )  "T" ")" )); end; 






:: deftheorem    defines :::"|^"::: YELLOW_1:def 5 :  (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "T")) "being"    ($#l1_orders_2 :::"RelStr"::: )   "holds"  (Bool (Set (Set (Var "T"))  ($#k6_yellow_1 :::"|^"::: )  (Set (Var "I")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_yellow_1 :::"product"::: )  (Set  "(" (Set (Var "I"))  ($#k7_funcop_1 :::"-->"::: )  (Set (Var "T")) ")" ))))); 
 
theorem :: YELLOW_1:26 (Bool  "for" (Set (Var "J")) "being"   ($#v1_yellow_1 :::"RelStr-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set   ($#k1_xboole_0 :::"{}"::: )  ) "holds"  (Bool (Set   ($#k5_yellow_1 :::"product"::: )  (Set (Var "J")))  ($#r1_hidden :::"="::: )  (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set  "("  ($#k6_partfun1 :::"id"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) "#)" ))) ; 
 
theorem :: YELLOW_1:27 (Bool  "for" (Set (Var "Y")) "being"    ($#l1_orders_2 :::"RelStr"::: )   "holds"  (Bool (Set (Set (Var "Y"))  ($#k6_yellow_1 :::"|^"::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set  "("  ($#k6_partfun1 :::"id"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) "#)" ))) ; 
 
theorem :: YELLOW_1:28 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Y")) "being"    ($#l1_orders_2 :::"RelStr"::: )   "holds"  (Bool (Set   ($#k1_funct_2 :::"Funcs"::: )   "(" (Set (Var "X")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "Y"))) ")" )  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "(" (Set (Var "Y"))  ($#k6_yellow_1 :::"|^"::: )  (Set (Var "X")) ")" ))))) ; 
 registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; let "Y" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; 
cluster (Set "Y"  ($#k6_yellow_1 :::"|^"::: )  "X") ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_orders_2 :::"strict"::: )   ; 
end; registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; let "Y" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; 
cluster (Set "Y"  ($#k6_yellow_1 :::"|^"::: )  "X") ->   ($#v1_orders_2 :::"strict"::: )     ($#v3_orders_2 :::"reflexive"::: )   ; 
end; registrationlet "Y" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; 
cluster (Set "Y"  ($#k6_yellow_1 :::"|^"::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) )) -> (Num 1)  ($#v13_struct_0 :::"-element"::: )     ($#v1_orders_2 :::"strict"::: )   ; 
end; registrationlet "Y" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; 
cluster (Set "Y"  ($#k6_yellow_1 :::"|^"::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) )) ->   ($#v1_orders_2 :::"strict"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v1_lattice3 :::"with_suprema"::: )     ($#v2_lattice3 :::"with_infima"::: )   ; 
end; registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; let "Y" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v4_orders_2 :::"transitive"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; 
cluster (Set "Y"  ($#k6_yellow_1 :::"|^"::: )  "X") ->   ($#v1_orders_2 :::"strict"::: )     ($#v4_orders_2 :::"transitive"::: )   ; 
end; registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; let "Y" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v5_orders_2 :::"antisymmetric"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; 
cluster (Set "Y"  ($#k6_yellow_1 :::"|^"::: )  "X") ->   ($#v1_orders_2 :::"strict"::: )     ($#v5_orders_2 :::"antisymmetric"::: )   ; 
end; registrationlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "Y" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v5_orders_2 :::"antisymmetric"::: )     ($#v2_lattice3 :::"with_infima"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; 
cluster (Set "Y"  ($#k6_yellow_1 :::"|^"::: )  "X") ->   ($#v1_orders_2 :::"strict"::: )     ($#v2_lattice3 :::"with_infima"::: )   ; 
end; registrationlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "Y" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v5_orders_2 :::"antisymmetric"::: )     ($#v1_lattice3 :::"with_suprema"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; 
cluster (Set "Y"  ($#k6_yellow_1 :::"|^"::: )  "X") ->   ($#v1_orders_2 :::"strict"::: )     ($#v1_lattice3 :::"with_suprema"::: )   ; 
end; definitionlet "S", "T" be    ($#l1_orders_2 :::"RelStr"::: )  ; func  :::"MonMaps":::  "(" "S" "," "T" ")"  ->   ($#v1_orders_2 :::"strict"::: )     ($#v4_yellow_0 :::"full"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set "T"  ($#k6_yellow_1 :::"|^"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S")) means :: YELLOW_1:def 6 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" "S" "," "T" "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)) "iff" (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_funct_2 :::"Funcs"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T") ")" )) & (Bool (Set (Var "f")) "is"   ($#v5_orders_3 :::"monotone"::: )  )  ")" )  ")" )); end; 






:: deftheorem    defines :::"MonMaps"::: YELLOW_1:def 6 :  (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "b3")) "being"   ($#v1_orders_2 :::"strict"::: )     ($#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")))) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_yellow_1 :::"MonMaps"::: )   "(" (Set (Var "S")) "," (Set (Var "T")) ")" )) "iff" (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b3")))) "iff" (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_funct_2 :::"Funcs"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) ")" )) & (Bool (Set (Var "f")) "is"   ($#v5_orders_3 :::"monotone"::: )  )  ")" )  ")" ))  ")" )));