:: WAYBEL13  semantic presentation begin  
theorem :: WAYBEL13:1 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v4_orders_2 :::"transitive"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "x"))  ($#r3_orders_2 :::"<="::: )  (Set (Var "y")))) "holds"  (Bool (Set   ($#k2_waybel_8 :::"compactbelow"::: )  (Set (Var "x")))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_waybel_8 :::"compactbelow"::: )  (Set (Var "y")))))) ; 
 
theorem :: WAYBEL13:2 (Bool  "for" (Set (Var "L")) "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 "L")) "holds"  (Bool (Set   ($#k2_waybel_8 :::"compactbelow"::: )  (Set (Var "x"))) "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_waybel_8 :::"CompactSublatt"::: )  (Set (Var "L")) ")" )))) ; 
 
theorem :: WAYBEL13:3 (Bool  "for" (Set (Var "L")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "S")) "being"    ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set (Var "L"))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds"  (Bool (Set (Var "X")) "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")))))) ; 
 
theorem :: WAYBEL13:4 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v4_orders_2 :::"transitive"::: )     ($#v1_lattice3 :::"with_suprema"::: )     ($#l1_orders_2 :::"RelStr"::: )   "holds"  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L"))) "is"   ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L")))) ; 
 
theorem :: WAYBEL13:5 (Bool  "for" (Set (Var "L1")) "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"::: )    (Bool  "for" (Set (Var "L2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#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"))) "#)" )) & (Bool (Set (Var "L1")) "is"   ($#v24_waybel_0 :::"up-complete"::: )  )) "holds"  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k1_waybel_8 :::"CompactSublatt"::: )  (Set (Var "L1")) ")" ))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k1_waybel_8 :::"CompactSublatt"::: )  (Set (Var "L2")) ")" ))))) ; 
 begin  
theorem :: WAYBEL13:6 (Bool  "for" (Set (Var "L")) "being"   ($#v1_yellow_0 :::"lower-bounded"::: )     ($#v2_waybel_8 :::"algebraic"::: )    ($#l1_orders_2 :::"LATTICE":::)  (Bool  "for" (Set (Var "S")) "being"   ($#m1_yellow_0 :::"CLSubFrame":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Var "S")) "is"   ($#v2_waybel_8 :::"algebraic"::: )  ))) ; 
 
theorem :: WAYBEL13:7 (Bool  "for" (Set (Var "X")) "," (Set (Var "E")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "L")) "being"   ($#m1_yellow_0 :::"CLSubFrame":::) "of" (Set   ($#k3_yellow_1 :::"BoolePoset"::: )  (Set (Var "X"))) "holds"   (Bool  "("  (Bool (Set (Var "E"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k1_waybel_8 :::"CompactSublatt"::: )  (Set (Var "L")) ")" ))) "iff" (Bool  "ex" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k3_yellow_1 :::"BoolePoset"::: )  (Set (Var "X")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v1_finset_1 :::"finite"::: )  ) & (Bool (Set (Var "E"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_setfam_1 :::"meet"::: )   "{"  (Set (Var "Y")) where Y "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Var "F"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))  "}"  )) & (Bool (Set (Var "F"))  ($#r1_tarski :::"c="::: )  (Set (Var "E")))  ")" ))  ")" ))) ; 
 
theorem :: WAYBEL13:8 (Bool  "for" (Set (Var "L")) "being"   ($#v1_yellow_0 :::"lower-bounded"::: )    ($#l1_orders_2 :::"sup-Semilattice":::) "holds"  (Bool (Set   ($#k2_yellow_1 :::"InclPoset"::: )  (Set  "("  ($#k7_waybel_0 :::"Ids"::: )  (Set (Var "L")) ")" )) "is"   ($#m1_yellow_0 :::"CLSubFrame":::) "of" (Set   ($#k3_yellow_1 :::"BoolePoset"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))))) ; 
 registrationlet "L" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v4_orders_2 :::"transitive"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_waybel_0 :::"directed"::: )     ($#v12_waybel_0 :::"lower"::: )     ($#v14_waybel_0 :::"principal"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "L"))); 
end; 
theorem :: WAYBEL13:9 (Bool  "for" (Set (Var "L")) "being"   ($#v1_yellow_0 :::"lower-bounded"::: )    ($#l1_orders_2 :::"sup-Semilattice":::)  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_waybel_0 :::"directed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k2_yellow_1 :::"InclPoset"::: )  (Set  "("  ($#k7_waybel_0 :::"Ids"::: )  (Set (Var "L")) ")" ) ")" ) "holds"  (Bool (Set   ($#k1_yellow_0 :::"sup"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "X")))))) ; 
 
theorem :: WAYBEL13:10 (Bool  "for" (Set (Var "S")) "being"   ($#v1_yellow_0 :::"lower-bounded"::: )    ($#l1_orders_2 :::"sup-Semilattice":::) "holds"  (Bool (Set   ($#k2_yellow_1 :::"InclPoset"::: )  (Set  "("  ($#k7_waybel_0 :::"Ids"::: )  (Set (Var "S")) ")" )) "is"   ($#v2_waybel_8 :::"algebraic"::: )  )) ; 
 
theorem :: WAYBEL13:11 (Bool  "for" (Set (Var "S")) "being"   ($#v1_yellow_0 :::"lower-bounded"::: )    ($#l1_orders_2 :::"sup-Semilattice":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k2_yellow_1 :::"InclPoset"::: )  (Set  "("  ($#k7_waybel_0 :::"Ids"::: )  (Set (Var "S")) ")" ) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "x")) "is"   ($#v1_waybel_3 :::"compact"::: )  ) "iff" (Bool (Set (Var "x")) "is"   ($#v14_waybel_0 :::"principal"::: )    ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "S")))  ")" ))) ; 
 
theorem :: WAYBEL13:12 (Bool  "for" (Set (Var "S")) "being"   ($#v1_yellow_0 :::"lower-bounded"::: )    ($#l1_orders_2 :::"sup-Semilattice":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k2_yellow_1 :::"InclPoset"::: )  (Set  "("  ($#k7_waybel_0 :::"Ids"::: )  (Set (Var "S")) ")" ) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "x")) "is"   ($#v1_waybel_3 :::"compact"::: )  ) "iff" (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_waybel_0 :::"downarrow"::: )  (Set (Var "a")))))  ")" ))) ; 
 
theorem :: WAYBEL13:13 (Bool  "for" (Set (Var "L")) "being"   ($#v1_yellow_0 :::"lower-bounded"::: )    ($#l1_orders_2 :::"sup-Semilattice":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set  "("  ($#k1_waybel_8 :::"CompactSublatt"::: )  (Set  "("  ($#k2_yellow_1 :::"InclPoset"::: )  (Set  "("  ($#k7_waybel_0 :::"Ids"::: )  (Set (Var "L")) ")" ) ")" ) ")" )  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_waybel_0 :::"downarrow"::: )  (Set (Var "x"))))  ")" )) "holds"  (Bool (Set (Var "f")) "is"   ($#v23_waybel_0 :::"isomorphic"::: )  ))) ; 
 
theorem :: WAYBEL13:14 (Bool  "for" (Set (Var "S")) "being"   ($#v1_yellow_0 :::"lower-bounded"::: )    ($#l1_orders_2 :::"LATTICE":::) "holds"  (Bool (Set   ($#k2_yellow_1 :::"InclPoset"::: )  (Set  "("  ($#k7_waybel_0 :::"Ids"::: )  (Set (Var "S")) ")" )) "is"   ($#v3_waybel_8 :::"arithmetic"::: )  )) ; 
 
theorem :: WAYBEL13:15 (Bool  "for" (Set (Var "L")) "being"   ($#v1_yellow_0 :::"lower-bounded"::: )    ($#l1_orders_2 :::"sup-Semilattice":::) "holds"  (Bool (Set   ($#k1_waybel_8 :::"CompactSublatt"::: )  (Set (Var "L"))) "is"   ($#v1_yellow_0 :::"lower-bounded"::: )    ($#l1_orders_2 :::"sup-Semilattice":::))) ; 
 
theorem :: WAYBEL13:16 (Bool  "for" (Set (Var "L")) "being"   ($#v1_yellow_0 :::"lower-bounded"::: )     ($#v2_waybel_8 :::"algebraic"::: )    ($#l1_orders_2 :::"sup-Semilattice":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set  "("  ($#k2_yellow_1 :::"InclPoset"::: )  (Set  "("  ($#k7_waybel_0 :::"Ids"::: )  (Set  "("  ($#k1_waybel_8 :::"CompactSublatt"::: )  (Set (Var "L")) ")" ) ")" ) ")" )  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_waybel_8 :::"compactbelow"::: )  (Set (Var "x"))))  ")" )) "holds"  (Bool (Set (Var "f")) "is"   ($#v23_waybel_0 :::"isomorphic"::: )  ))) ; 
 
theorem :: WAYBEL13:17 (Bool  "for" (Set (Var "L")) "being"   ($#v1_yellow_0 :::"lower-bounded"::: )     ($#v2_waybel_8 :::"algebraic"::: )    ($#l1_orders_2 :::"sup-Semilattice":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"   (Bool  "("  (Bool (Set   ($#k2_waybel_8 :::"compactbelow"::: )  (Set (Var "x"))) "is"   ($#v14_waybel_0 :::"principal"::: )    ($#m1_subset_1 :::"Ideal":::) "of" (Set  "("  ($#k1_waybel_8 :::"CompactSublatt"::: )  (Set (Var "L")) ")" )) "iff" (Bool (Set (Var "x")) "is"   ($#v1_waybel_3 :::"compact"::: )  )  ")" ))) ; 
 begin  
theorem :: WAYBEL13: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 "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L1"))  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L1")) "," (Set (Var "L2"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v23_waybel_0 :::"isomorphic"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_lattice3 :::"is_<=_than"::: )  (Set (Var "X"))) "iff" (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_lattice3 :::"is_<=_than"::: )  (Set (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "X"))))  ")" ))))) ; 
 
theorem :: WAYBEL13:19 (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 "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L1"))  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L1")) "," (Set (Var "L2"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v23_waybel_0 :::"isomorphic"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_lattice3 :::"is_>=_than"::: )  (Set (Var "X"))) "iff" (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r2_lattice3 :::"is_>=_than"::: )  (Set (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "X"))))  ")" ))))) ; 
 
theorem :: WAYBEL13:20 (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v5_orders_2 :::"antisymmetric"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L1")) "," (Set (Var "L2"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v23_waybel_0 :::"isomorphic"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v17_waybel_0 :::"infs-preserving"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v18_waybel_0 :::"sups-preserving"::: )  )  ")" ))) ; 
 registrationlet "L1", "L2" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v5_orders_2 :::"antisymmetric"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; 
cluster   ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FUNCT_2((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "L1") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "L2"))   ($#v23_waybel_0 :::"isomorphic"::: )    ->   ($#v17_waybel_0 :::"infs-preserving"::: )     ($#v18_waybel_0 :::"sups-preserving"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "L1") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "L2"))))); 
end; 
theorem :: WAYBEL13:21 (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "," (Set (Var "L3")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v4_orders_2 :::"transitive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L1")) "," (Set (Var "L2"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v17_waybel_0 :::"infs-preserving"::: )  ) & (Bool (Set (Var "L2")) "is"   ($#v4_yellow_0 :::"full"::: )     ($#v7_yellow_0 :::"infs-inheriting"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set (Var "L3"))) & (Bool (Set (Var "L3")) "is"   ($#v3_lattice3 :::"complete"::: )  )) "holds"  (Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L1")) "," (Set (Var "L3")) "st"  (Bool  "("  (Bool (Set (Var "f"))  ($#r8_pboole :::"="::: )  (Set (Var "g"))) & (Bool (Set (Var "g")) "is"   ($#v17_waybel_0 :::"infs-preserving"::: )  )  ")" )))) ; 
 
theorem :: WAYBEL13:22 (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "," (Set (Var "L3")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v4_orders_2 :::"transitive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L1")) "," (Set (Var "L2"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v5_orders_3 :::"monotone"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v22_waybel_0 :::"directed-sups-preserving"::: )  ) & (Bool (Set (Var "L2")) "is"   ($#v4_yellow_0 :::"full"::: )     ($#v4_waybel_0 :::"directed-sups-inheriting"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set (Var "L3"))) & (Bool (Set (Var "L3")) "is"   ($#v3_lattice3 :::"complete"::: )  )) "holds"  (Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L1")) "," (Set (Var "L3")) "st"  (Bool  "("  (Bool (Set (Var "f"))  ($#r8_pboole :::"="::: )  (Set (Var "g"))) & (Bool (Set (Var "g")) "is"   ($#v22_waybel_0 :::"directed-sups-preserving"::: )  )  ")" )))) ; 
 
theorem :: WAYBEL13:23 (Bool  "for" (Set (Var "L")) "being"   ($#v1_yellow_0 :::"lower-bounded"::: )    ($#l1_orders_2 :::"sup-Semilattice":::) "holds"  (Bool (Set   ($#k2_yellow_1 :::"InclPoset"::: )  (Set  "("  ($#k7_waybel_0 :::"Ids"::: )  (Set  "("  ($#k1_waybel_8 :::"CompactSublatt"::: )  (Set (Var "L")) ")" ) ")" )) "is"   ($#m1_yellow_0 :::"CLSubFrame":::) "of" (Set   ($#k3_yellow_1 :::"BoolePoset"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k1_waybel_8 :::"CompactSublatt"::: )  (Set (Var "L")) ")" ))))) ; 
 
theorem :: WAYBEL13:24 (Bool  "for" (Set (Var "L")) "being"   ($#v1_yellow_0 :::"lower-bounded"::: )     ($#v2_waybel_8 :::"algebraic"::: )    ($#l1_orders_2 :::"LATTICE":::) (Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set  "("  ($#k3_yellow_1 :::"BoolePoset"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k1_waybel_8 :::"CompactSublatt"::: )  (Set (Var "L")) ")" )) ")" ) "st"  (Bool  "("  (Bool (Set (Var "g")) "is"   ($#v17_waybel_0 :::"infs-preserving"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v22_waybel_0 :::"directed-sups-preserving"::: )  ) & (Bool (Set (Var "g")) "is" bbbadV2_FUNCT_1()) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_waybel_8 :::"compactbelow"::: )  (Set (Var "x"))))  ")" )  ")" ))) ; 
 
theorem :: WAYBEL13:25 (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"   ($#v1_yellow_0 :::"lower-bounded"::: )     ($#v2_waybel_8 :::"algebraic"::: )    ($#l1_orders_2 :::"LATTICE":::))  ")" )) "holds"  (Bool (Set   ($#k5_yellow_1 :::"product"::: )  (Set (Var "J"))) "is"   ($#v1_yellow_0 :::"lower-bounded"::: )     ($#v2_waybel_8 :::"algebraic"::: )    ($#l1_orders_2 :::"LATTICE":::)))) ; 
 
theorem :: WAYBEL13:26 (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#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 "L1")) "," (Set (Var "L2"))  ($#r5_waybel_1 :::"are_isomorphic"::: )  )) ; 
 
theorem :: WAYBEL13:27 (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v24_waybel_0 :::"up-complete"::: )    ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L1")) "," (Set (Var "L2"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v23_waybel_0 :::"isomorphic"::: )  )) "holds"  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1")) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_waybel_3 :::"<<"::: )  (Set (Var "y"))) "iff" (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_waybel_3 :::"<<"::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "y"))))  ")" )))) ; 
 
theorem :: WAYBEL13:28 (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v24_waybel_0 :::"up-complete"::: )    ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L1")) "," (Set (Var "L2"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v23_waybel_0 :::"isomorphic"::: )  )) "holds"  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1")) "holds"   (Bool  "("  (Bool (Set (Var "x")) "is"   ($#v1_waybel_3 :::"compact"::: )  ) "iff" (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x"))) "is"   ($#v1_waybel_3 :::"compact"::: )  )  ")" )))) ; 
 
theorem :: WAYBEL13:29 (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v24_waybel_0 :::"up-complete"::: )    ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L1")) "," (Set (Var "L2"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v23_waybel_0 :::"isomorphic"::: )  )) "holds"  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1")) "holds"  (Bool (Set (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set  "("  ($#k2_waybel_8 :::"compactbelow"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_waybel_8 :::"compactbelow"::: )  (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" )))))) ; 
 
theorem :: WAYBEL13:30 (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_orders_2 :::"Poset":::)  "st" (Bool (Bool (Set (Var "L1")) "," (Set (Var "L2"))  ($#r5_waybel_1 :::"are_isomorphic"::: )  ) & (Bool (Set (Var "L1")) "is"   ($#v24_waybel_0 :::"up-complete"::: )  )) "holds"  (Bool (Set (Var "L2")) "is"   ($#v24_waybel_0 :::"up-complete"::: )  )) ; 
 
theorem :: WAYBEL13:31 (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_orders_2 :::"Poset":::)  "st" (Bool (Bool (Set (Var "L1")) "," (Set (Var "L2"))  ($#r5_waybel_1 :::"are_isomorphic"::: )  ) & (Bool (Set (Var "L1")) "is"   ($#v3_lattice3 :::"complete"::: )  ) & (Bool (Set (Var "L1")) "is"   ($#v1_waybel_8 :::"satisfying_axiom_K"::: )  )) "holds"  (Bool (Set (Var "L2")) "is"   ($#v1_waybel_8 :::"satisfying_axiom_K"::: )  )) ; 
 
theorem :: WAYBEL13:32 (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"   ($#l1_orders_2 :::"sup-Semilattice":::)  "st" (Bool (Bool (Set (Var "L1")) "," (Set (Var "L2"))  ($#r5_waybel_1 :::"are_isomorphic"::: )  ) & (Bool (Set (Var "L1")) "is"   ($#v1_yellow_0 :::"lower-bounded"::: )  ) & (Bool (Set (Var "L1")) "is"   ($#v2_waybel_8 :::"algebraic"::: )  )) "holds"  (Bool (Set (Var "L2")) "is"   ($#v2_waybel_8 :::"algebraic"::: )  )) ; 
 
theorem :: WAYBEL13:33 (Bool  "for" (Set (Var "L")) "being"   ($#v1_yellow_0 :::"lower-bounded"::: )     ($#v3_waybel_3 :::"continuous"::: )    ($#l1_orders_2 :::"sup-Semilattice":::) "holds"   (Bool  "("  (Bool (Set   ($#k2_yellow_2 :::"SupMap"::: )  (Set (Var "L"))) "is"   ($#v17_waybel_0 :::"infs-preserving"::: )  ) & (Bool (Set   ($#k2_yellow_2 :::"SupMap"::: )  (Set (Var "L"))) "is"   ($#v18_waybel_0 :::"sups-preserving"::: )  )  ")" )) ; 
 
theorem :: WAYBEL13:34 (Bool  "for" (Set (Var "L")) "being"   ($#v1_yellow_0 :::"lower-bounded"::: )    ($#l1_orders_2 :::"LATTICE":::) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "L")) "is"   ($#v2_waybel_8 :::"algebraic"::: )  )) "implies" (Bool  "ex" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  (Bool  "ex" (Set (Var "S")) "being"   ($#v4_yellow_0 :::"full"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set   ($#k3_yellow_1 :::"BoolePoset"::: )  (Set (Var "X"))) "st"  (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v7_yellow_0 :::"infs-inheriting"::: )  ) & (Bool (Set (Var "S")) "is"   ($#v4_waybel_0 :::"directed-sups-inheriting"::: )  ) & (Bool (Set (Var "L")) "," (Set (Var "S"))  ($#r5_waybel_1 :::"are_isomorphic"::: )  )  ")" )))  ")"  &  "("  (Bool (Bool  "ex" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )  (Bool  "ex" (Set (Var "S")) "being"   ($#v4_yellow_0 :::"full"::: )     ($#m1_yellow_0 :::"SubRelStr"::: )   "of" (Set   ($#k3_yellow_1 :::"BoolePoset"::: )  (Set (Var "X"))) "st"  (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v7_yellow_0 :::"infs-inheriting"::: )  ) & (Bool (Set (Var "S")) "is"   ($#v4_waybel_0 :::"directed-sups-inheriting"::: )  ) & (Bool (Set (Var "L")) "," (Set (Var "S"))  ($#r5_waybel_1 :::"are_isomorphic"::: )  )  ")" )))) "implies" (Bool (Set (Var "L")) "is"   ($#v2_waybel_8 :::"algebraic"::: )  )  ")"   ")" )) ; 
 
theorem :: WAYBEL13:35 (Bool  "for" (Set (Var "L")) "being"   ($#v1_yellow_0 :::"lower-bounded"::: )    ($#l1_orders_2 :::"LATTICE":::) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "L")) "is"   ($#v2_waybel_8 :::"algebraic"::: )  )) "implies" (Bool  "ex" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  (Bool  "ex" (Set (Var "c")) "being"   ($#v7_waybel_1 :::"closure"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k3_yellow_1 :::"BoolePoset"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k3_yellow_1 :::"BoolePoset"::: )  (Set (Var "X")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "c")) "is"   ($#v22_waybel_0 :::"directed-sups-preserving"::: )  ) & (Bool (Set (Var "L")) "," (Set   ($#k1_yellow_2 :::"Image"::: )  (Set (Var "c")))  ($#r5_waybel_1 :::"are_isomorphic"::: )  )  ")" )))  ")"  &  "("  (Bool (Bool  "ex" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )  (Bool  "ex" (Set (Var "c")) "being"   ($#v7_waybel_1 :::"closure"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k3_yellow_1 :::"BoolePoset"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k3_yellow_1 :::"BoolePoset"::: )  (Set (Var "X")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "c")) "is"   ($#v22_waybel_0 :::"directed-sups-preserving"::: )  ) & (Bool (Set (Var "L")) "," (Set   ($#k1_yellow_2 :::"Image"::: )  (Set (Var "c")))  ($#r5_waybel_1 :::"are_isomorphic"::: )  )  ")" )))) "implies" (Bool (Set (Var "L")) "is"   ($#v2_waybel_8 :::"algebraic"::: )  )  ")"   ")" )) ;