:: LATTICE3  semantic presentation begin  definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; func  :::"BooleLatt"::: "X" ->   ($#v3_lattices :::"strict"::: )     ($#l3_lattices :::"LattStr"::: )   means :: LATTICE3:def 1 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set   ($#k9_setfam_1 :::"bool"::: )  "X")) & (Bool  "("   "for" (Set (Var "Y")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "X" "holds"   (Bool  "("  (Bool (Set (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" it)  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "Y")) "," (Set (Var "Z")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "Y"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "Z")))) & (Bool (Set (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" it)  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "Y")) "," (Set (Var "Z")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "Y"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "Z"))))  ")" )  ")" )  ")" ); end; 





:: deftheorem    defines :::"BooleLatt"::: LATTICE3:def 1 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#v3_lattices :::"strict"::: )     ($#l3_lattices :::"LattStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_lattice3 :::"BooleLatt"::: )  (Set (Var "X")))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set   ($#k9_setfam_1 :::"bool"::: )  (Set (Var "X")))) & (Bool  "("   "for" (Set (Var "Y")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" (Set (Var "b2")))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "Y")) "," (Set (Var "Z")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "Y"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "Z")))) & (Bool (Set (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set (Var "b2")))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "Y")) "," (Set (Var "Z")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "Y"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "Z"))))  ")" )  ")" )  ")" )  ")" ))); 
 










registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k1_lattice3 :::"BooleLatt"::: )  "X") ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_lattices :::"strict"::: )   ; 
end; registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; let "x", "y" be   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k1_lattice3 :::"BooleLatt"::: )  (Set (Const "X")) ")" ); let "x9", "y9" be    ($#m1_hidden :::"set"::: )  ; 
identify ; 

identify ; 
end; 
theorem :: LATTICE3:1 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k1_lattice3 :::"BooleLatt"::: )  (Set (Var "X")) ")" ) "holds"   (Bool  "("  (Bool (Set (Set (Var "x"))  ($#k1_lattices :::""\/""::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "y")))) & (Bool (Set (Set (Var "x"))  ($#k2_lattices :::""/\""::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "y"))))  ")" ))) ; 
 
theorem :: LATTICE3: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  "("  ($#k1_lattice3 :::"BooleLatt"::: )  (Set (Var "X")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_lattices :::"[="::: )  (Set (Var "y"))) "iff" (Bool (Set (Var "x"))  ($#r1_tarski :::"c="::: )  (Set (Var "y")))  ")" ))) ; 
 registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k1_lattice3 :::"BooleLatt"::: )  "X") ->   ($#v3_lattices :::"strict"::: )     ($#v10_lattices :::"Lattice-like"::: )   ; 
end; 



theorem :: LATTICE3:3 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k1_lattice3 :::"BooleLatt"::: )  (Set (Var "X"))) "is"   ($#v13_lattices :::"lower-bounded"::: )  ) & (Bool (Set   ($#k5_lattices :::"Bottom"::: )  (Set  "("  ($#k1_lattice3 :::"BooleLatt"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )) ; 
 
theorem :: LATTICE3:4 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k1_lattice3 :::"BooleLatt"::: )  (Set (Var "X"))) "is"   ($#v14_lattices :::"upper-bounded"::: )  ) & (Bool (Set   ($#k6_lattices :::"Top"::: )  (Set  "("  ($#k1_lattice3 :::"BooleLatt"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "X")))  ")" )) ; 
 registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k1_lattice3 :::"BooleLatt"::: )  "X") ->   ($#v3_lattices :::"strict"::: )     ($#v17_lattices :::"Boolean"::: )   ; 
end; 
theorem :: LATTICE3:5 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k1_lattice3 :::"BooleLatt"::: )  (Set (Var "X")) ")" ) "holds"  (Bool (Set (Set (Var "x"))  ($#k7_lattices :::"`"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k6_subset_1 :::"\"::: )  (Set (Var "x")))))) ; 
 begin  definitionlet "L" be   ($#l3_lattices :::"Lattice":::); :: original: :::"LattRel"::: redefine func  :::"LattRel"::: "L" ->   ($#m1_subset_1 :::"Order":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "L"); end; definitionlet "L" be   ($#l3_lattices :::"Lattice":::); func  :::"LattPOSet"::: "L" ->   ($#v1_orders_2 :::"strict"::: )    ($#l1_orders_2 :::"Poset":::) equals :: LATTICE3:def 2 (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "L") "," (Set  "("  ($#k2_lattice3 :::"LattRel"::: )  "L" ")" ) "#)" ); end; 





:: deftheorem    defines :::"LattPOSet"::: LATTICE3:def 2 :  (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::) "holds"  (Bool (Set   ($#k3_lattice3 :::"LattPOSet"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L"))) "," (Set  "("  ($#k2_lattice3 :::"LattRel"::: )  (Set (Var "L")) ")" ) "#)" ))); 
 registrationlet "L" be   ($#l3_lattices :::"Lattice":::); 
cluster (Set   ($#k3_lattice3 :::"LattPOSet"::: )  "L") ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_orders_2 :::"strict"::: )   ; 
end; 
theorem :: LATTICE3:6 (Bool  "for" (Set (Var "L1")) "," (Set (Var "L2")) "being"   ($#l3_lattices :::"Lattice":::)  "st" (Bool (Bool (Set   ($#k3_lattice3 :::"LattPOSet"::: )  (Set (Var "L1")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_lattice3 :::"LattPOSet"::: )  (Set (Var "L2"))))) "holds"  (Bool (Set   ($#g3_lattices :::"LattStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L1"))) "," (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" (Set (Var "L1"))) "," (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set (Var "L1"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g3_lattices :::"LattStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L2"))) "," (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" (Set (Var "L2"))) "," (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set (Var "L2"))) "#)" ))) ; 
 definitionlet "L" be   ($#l3_lattices :::"Lattice":::); let "p" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); func "p" :::"%":::  ->   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k3_lattice3 :::"LattPOSet"::: )  "L" ")" ) equals :: LATTICE3:def 3 "p"; end; 






:: deftheorem    defines :::"%"::: LATTICE3:def 3 :  (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "p"))  ($#k4_lattice3 :::"%"::: )  )  ($#r1_hidden :::"="::: )  (Set (Var "p"))))); 
 definitionlet "L" be   ($#l3_lattices :::"Lattice":::); let "p" be   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k3_lattice3 :::"LattPOSet"::: )  (Set (Const "L")) ")" ); func  :::"%"::: "p" ->   ($#m1_subset_1 :::"Element":::) "of" "L" equals :: LATTICE3:def 4 "p"; end; 






:: deftheorem    defines :::"%"::: LATTICE3:def 4 :  (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k3_lattice3 :::"LattPOSet"::: )  (Set (Var "L")) ")" ) "holds"  (Bool (Set   ($#k5_lattice3 :::"%"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "p"))))); 
 







theorem :: LATTICE3:7 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"   (Bool  "("  (Bool (Set (Var "p"))  ($#r3_lattices :::"[="::: )  (Set (Var "q"))) "iff" (Bool (Set (Set (Var "p"))  ($#k4_lattice3 :::"%"::: )  )  ($#r3_orders_2 :::"<="::: )  (Set (Set (Var "q"))  ($#k4_lattice3 :::"%"::: )  ))  ")" ))) ; 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "O" be   ($#m1_subset_1 :::"Order":::) "of" (Set (Const "X")); :: original: :::"~"::: redefine func "O" :::"~":::  ->   ($#m1_subset_1 :::"Order":::) "of" "X"; end; definitionlet "A" be    ($#l1_orders_2 :::"RelStr"::: )  ; func "A" :::"~":::  ->   ($#v1_orders_2 :::"strict"::: )     ($#l1_orders_2 :::"RelStr"::: )   equals :: LATTICE3:def 5 (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "A") "," (Set  "(" (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "A")  ($#k3_relset_1 :::"~"::: )  ")" ) "#)" ); end; 





:: deftheorem    defines :::"~"::: LATTICE3:def 5 :  (Bool  "for" (Set (Var "A")) "being"    ($#l1_orders_2 :::"RelStr"::: )   "holds"  (Bool (Set (Set (Var "A"))  ($#k7_lattice3 :::"~"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "A"))) "," (Set  "(" (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "A")))  ($#k3_relset_1 :::"~"::: )  ")" ) "#)" ))); 
 registrationlet "A" be   ($#l1_orders_2 :::"Poset":::); 
cluster (Set "A"  ($#k7_lattice3 :::"~"::: )  ) ->   ($#v1_orders_2 :::"strict"::: )     ($#v3_orders_2 :::"reflexive"::: )     ($#v4_orders_2 :::"transitive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )   ; 
end; registrationlet "A" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; 
cluster (Set "A"  ($#k7_lattice3 :::"~"::: )  ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_orders_2 :::"strict"::: )   ; 
end; 








theorem :: LATTICE3:8 (Bool  "for" (Set (Var "A")) "being"    ($#l1_orders_2 :::"RelStr"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k7_lattice3 :::"~"::: )  ")" )  ($#k7_lattice3 :::"~"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "A"))) "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "A"))) "#)" ))) ; 
 definitionlet "A" be    ($#l1_orders_2 :::"RelStr"::: )  ; let "a" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "A")); func "a" :::"~":::  ->   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" "A"  ($#k7_lattice3 :::"~"::: )  ")" ) equals :: LATTICE3:def 6 "a"; end; 






:: deftheorem    defines :::"~"::: LATTICE3:def 6 :  (Bool  "for" (Set (Var "A")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds"  (Bool (Set (Set (Var "a"))  ($#k8_lattice3 :::"~"::: )  )  ($#r1_hidden :::"="::: )  (Set (Var "a"))))); 
 definitionlet "A" be    ($#l1_orders_2 :::"RelStr"::: )  ; let "a" be   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Const "A"))  ($#k7_lattice3 :::"~"::: )  ")" ); func  :::"~"::: "a" ->   ($#m1_subset_1 :::"Element":::) "of" "A" equals :: LATTICE3:def 7 "a"; end; 






:: deftheorem    defines :::"~"::: LATTICE3:def 7 :  (Bool  "for" (Set (Var "A")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Var "A"))  ($#k7_lattice3 :::"~"::: )  ")" ) "holds"  (Bool (Set   ($#k9_lattice3 :::"~"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "a"))))); 
 
theorem :: LATTICE3:9 (Bool  "for" (Set (Var "A")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds"   (Bool  "("  (Bool (Set (Var "a"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "b"))) "iff" (Bool (Set (Set (Var "b"))  ($#k8_lattice3 :::"~"::: )  )  ($#r1_orders_2 :::"<="::: )  (Set (Set (Var "a"))  ($#k8_lattice3 :::"~"::: )  ))  ")" ))) ; 
 definitionlet "A" be    ($#l1_orders_2 :::"RelStr"::: )  ; let "X" be    ($#m1_hidden :::"set"::: )  ; let "a" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "A")); pred "a" :::"is_<=_than"::: "X" means :: LATTICE3:def 8 (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" "A"  "st" (Bool (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  "X")) "holds"  (Bool "a"  ($#r1_orders_2 :::"<="::: )  (Set (Var "b")))); pred "X" :::"is_<=_than"::: "a" means :: LATTICE3:def 9 (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" "A"  "st" (Bool (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  "X")) "holds"  (Bool (Set (Var "b"))  ($#r1_orders_2 :::"<="::: )  "a")); end; 












:: deftheorem    defines :::"is_<=_than"::: LATTICE3:def 8 :  (Bool  "for" (Set (Var "A")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds"   (Bool  "("  (Bool (Set (Var "a"))  ($#r1_lattice3 :::"is_<=_than"::: )  (Set (Var "X"))) "iff" (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "a"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "b"))))  ")" )))); 
 
:: deftheorem    defines :::"is_<=_than"::: LATTICE3:def 9 :  (Bool  "for" (Set (Var "A")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r2_lattice3 :::"is_<=_than"::: )  (Set (Var "a"))) "iff" (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "b"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "a"))))  ")" )))); 
 notationlet "A" be    ($#l1_orders_2 :::"RelStr"::: )  ; let "X" be    ($#m1_hidden :::"set"::: )  ; let "a" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "A")); synonym "X" :::"is_>=_than"::: "a" for "a" :::"is_<=_than"::: "X"; synonym "a" :::"is_>=_than"::: "X" for "X" :::"is_<=_than"::: "a"; end; definitionlet "IT" be    ($#l1_orders_2 :::"RelStr"::: )  ; attr "IT" is  :::"with_suprema":::  means :: LATTICE3:def 10 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT" (Bool  "ex" (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT" "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "z"))) & (Bool (Set (Var "y"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "z"))) & (Bool  "("   "for" (Set (Var "z9")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT"  "st" (Bool (Bool (Set (Var "x"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "z9"))) & (Bool (Set (Var "y"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "z9")))) "holds"  (Bool (Set (Var "z"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "z9")))  ")" )  ")" ))); attr "IT" is  :::"with_infima":::  means :: LATTICE3:def 11 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT" (Bool  "ex" (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT" "st"  (Bool  "("  (Bool (Set (Var "z"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "x"))) & (Bool (Set (Var "z"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "y"))) & (Bool  "("   "for" (Set (Var "z9")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT"  "st" (Bool (Bool (Set (Var "z9"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "x"))) & (Bool (Set (Var "z9"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "y")))) "holds"  (Bool (Set (Var "z9"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "z")))  ")" )  ")" ))); end; 








:: deftheorem    defines :::"with_suprema"::: LATTICE3:def 10 :  (Bool  "for" (Set (Var "IT")) "being"    ($#l1_orders_2 :::"RelStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_lattice3 :::"with_suprema"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) (Bool  "ex" (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "z"))) & (Bool (Set (Var "y"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "z"))) & (Bool  "("   "for" (Set (Var "z9")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT"))  "st" (Bool (Bool (Set (Var "x"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "z9"))) & (Bool (Set (Var "y"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "z9")))) "holds"  (Bool (Set (Var "z"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "z9")))  ")" )  ")" )))  ")" )); 
 
:: deftheorem    defines :::"with_infima"::: LATTICE3:def 11 :  (Bool  "for" (Set (Var "IT")) "being"    ($#l1_orders_2 :::"RelStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v2_lattice3 :::"with_infima"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) (Bool  "ex" (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st"  (Bool  "("  (Bool (Set (Var "z"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "x"))) & (Bool (Set (Var "z"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "y"))) & (Bool  "("   "for" (Set (Var "z9")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT"))  "st" (Bool (Bool (Set (Var "z9"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "x"))) & (Bool (Set (Var "z9"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "y")))) "holds"  (Bool (Set (Var "z9"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "z")))  ")" )  ")" )))  ")" )); 
 registration
cluster   ($#v1_lattice3 :::"with_suprema"::: )    ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   for    ($#l1_orders_2 :::"RelStr"::: )  ; 

cluster   ($#v2_lattice3 :::"with_infima"::: )    ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   for    ($#l1_orders_2 :::"RelStr"::: )  ; 
end; 
theorem :: LATTICE3:10 (Bool  "for" (Set (Var "A")) "being"    ($#l1_orders_2 :::"RelStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v1_lattice3 :::"with_suprema"::: )  ) "iff" (Bool (Set (Set (Var "A"))  ($#k7_lattice3 :::"~"::: )  ) "is"   ($#v2_lattice3 :::"with_infima"::: )  )  ")" )) ; 
 
theorem :: LATTICE3:11 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::) "holds"   (Bool  "("  (Bool (Set   ($#k3_lattice3 :::"LattPOSet"::: )  (Set (Var "L"))) "is"   ($#v1_lattice3 :::"with_suprema"::: )  ) & (Bool (Set   ($#k3_lattice3 :::"LattPOSet"::: )  (Set (Var "L"))) "is"   ($#v2_lattice3 :::"with_infima"::: )  )  ")" )) ; 
 definitionlet "IT" be    ($#l1_orders_2 :::"RelStr"::: )  ; attr "IT" is  :::"complete":::  means :: LATTICE3:def 12 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT" "st"  (Bool  "("  (Bool (Set (Var "X"))  ($#r2_lattice3 :::"is_<=_than"::: )  (Set (Var "a"))) & (Bool  "("   "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT"  "st" (Bool (Bool (Set (Var "X"))  ($#r2_lattice3 :::"is_<=_than"::: )  (Set (Var "b")))) "holds"  (Bool (Set (Var "a"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "b")))  ")" )  ")" ))); end; 




:: deftheorem    defines :::"complete"::: LATTICE3:def 12 :  (Bool  "for" (Set (Var "IT")) "being"    ($#l1_orders_2 :::"RelStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v3_lattice3 :::"complete"::: )  ) "iff" (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st"  (Bool  "("  (Bool (Set (Var "X"))  ($#r2_lattice3 :::"is_<=_than"::: )  (Set (Var "a"))) & (Bool  "("   "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT"))  "st" (Bool (Bool (Set (Var "X"))  ($#r2_lattice3 :::"is_<=_than"::: )  (Set (Var "b")))) "holds"  (Bool (Set (Var "a"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "b")))  ")" )  ")" )))  ")" )); 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_orders_2 :::"strict"::: )   bbbadV2_ORDERS_2()   ($#v3_orders_2 :::"reflexive"::: )     ($#v4_orders_2 :::"transitive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v3_lattice3 :::"complete"::: )    for    ($#l1_orders_2 :::"RelStr"::: )  ; 
end; 









theorem :: LATTICE3:12 (Bool  "for" (Set (Var "A")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    "st" (Bool (Bool (Set (Var "A")) "is"   ($#v3_lattice3 :::"complete"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v1_lattice3 :::"with_suprema"::: )  ) & (Bool (Set (Var "A")) "is"   ($#v2_lattice3 :::"with_infima"::: )  )  ")" )) ; 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_orders_2 :::"strict"::: )   bbbadV2_ORDERS_2()   ($#v3_orders_2 :::"reflexive"::: )     ($#v4_orders_2 :::"transitive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v1_lattice3 :::"with_suprema"::: )     ($#v2_lattice3 :::"with_infima"::: )     ($#v3_lattice3 :::"complete"::: )    for    ($#l1_orders_2 :::"RelStr"::: )  ; 
end; definitionlet "A" be    ($#l1_orders_2 :::"RelStr"::: )  ; assume 
(Bool (Set (Const "A")) "is"   ($#v5_orders_2 :::"antisymmetric"::: )  )
 ; let "a", "b" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "A")); assume 
(Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "A")) "st"  (Bool  "("  (Bool (Set (Const "a"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "x"))) & (Bool (Set (Const "b"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "x"))) & (Bool  "("   "for" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "A"))  "st" (Bool (Bool (Set (Const "a"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "c"))) & (Bool (Set (Const "b"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "c")))) "holds"  (Bool (Set (Var "x"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "c")))  ")" )  ")" ))
 ; func "a" :::""\/""::: "b" ->   ($#m1_subset_1 :::"Element":::) "of" "A" means :: LATTICE3:def 13 (Bool  "("  (Bool "a"  ($#r1_orders_2 :::"<="::: )  it) & (Bool "b"  ($#r1_orders_2 :::"<="::: )  it) & (Bool  "("   "for" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" "A"  "st" (Bool (Bool "a"  ($#r1_orders_2 :::"<="::: )  (Set (Var "c"))) & (Bool "b"  ($#r1_orders_2 :::"<="::: )  (Set (Var "c")))) "holds"  (Bool it  ($#r1_orders_2 :::"<="::: )  (Set (Var "c")))  ")" )  ")" ); end; 








:: deftheorem    defines :::""\/""::: LATTICE3:def 13 :  (Bool  "for" (Set (Var "A")) "being"    ($#l1_orders_2 :::"RelStr"::: )    "st" (Bool (Bool (Set (Var "A")) "is"   ($#v5_orders_2 :::"antisymmetric"::: )  )) "holds"  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A"))  "st" (Bool (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "x"))) & (Bool (Set (Var "b"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "x"))) & (Bool  "("   "for" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "c"))) & (Bool (Set (Var "b"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "c")))) "holds"  (Bool (Set (Var "x"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "c")))  ")" )  ")" ))) "holds"  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k10_lattice3 :::""\/""::: )  (Set (Var "b")))) "iff" (Bool  "("  (Bool (Set (Var "a"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "b4"))) & (Bool (Set (Var "b"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "b4"))) & (Bool  "("   "for" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "c"))) & (Bool (Set (Var "b"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "c")))) "holds"  (Bool (Set (Var "b4"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "c")))  ")" )  ")" )  ")" )))); 
 definitionlet "A" be    ($#l1_orders_2 :::"RelStr"::: )  ; assume 
(Bool (Set (Const "A")) "is"   ($#v5_orders_2 :::"antisymmetric"::: )  )
 ; let "a", "b" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "A")); assume 
(Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "A")) "st"  (Bool  "("  (Bool (Set (Const "a"))  ($#r1_orders_2 :::">="::: )  (Set (Var "x"))) & (Bool (Set (Const "b"))  ($#r1_orders_2 :::">="::: )  (Set (Var "x"))) & (Bool  "("   "for" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "A"))  "st" (Bool (Bool (Set (Const "a"))  ($#r1_orders_2 :::">="::: )  (Set (Var "c"))) & (Bool (Set (Const "b"))  ($#r1_orders_2 :::">="::: )  (Set (Var "c")))) "holds"  (Bool (Set (Var "x"))  ($#r1_orders_2 :::">="::: )  (Set (Var "c")))  ")" )  ")" ))
 ; func "a" :::""/\""::: "b" ->   ($#m1_subset_1 :::"Element":::) "of" "A" means :: LATTICE3:def 14 (Bool  "("  (Bool it  ($#r1_orders_2 :::"<="::: )  "a") & (Bool it  ($#r1_orders_2 :::"<="::: )  "b") & (Bool  "("   "for" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" "A"  "st" (Bool (Bool (Set (Var "c"))  ($#r1_orders_2 :::"<="::: )  "a") & (Bool (Set (Var "c"))  ($#r1_orders_2 :::"<="::: )  "b")) "holds"  (Bool (Set (Var "c"))  ($#r1_orders_2 :::"<="::: )  it)  ")" )  ")" ); end; 








:: deftheorem    defines :::""/\""::: LATTICE3:def 14 :  (Bool  "for" (Set (Var "A")) "being"    ($#l1_orders_2 :::"RelStr"::: )    "st" (Bool (Bool (Set (Var "A")) "is"   ($#v5_orders_2 :::"antisymmetric"::: )  )) "holds"  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A"))  "st" (Bool (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_orders_2 :::">="::: )  (Set (Var "x"))) & (Bool (Set (Var "b"))  ($#r1_orders_2 :::">="::: )  (Set (Var "x"))) & (Bool  "("   "for" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_orders_2 :::">="::: )  (Set (Var "c"))) & (Bool (Set (Var "b"))  ($#r1_orders_2 :::">="::: )  (Set (Var "c")))) "holds"  (Bool (Set (Var "x"))  ($#r1_orders_2 :::">="::: )  (Set (Var "c")))  ")" )  ")" ))) "holds"  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k11_lattice3 :::""/\""::: )  (Set (Var "b")))) "iff" (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "a"))) & (Bool (Set (Var "b4"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "b"))) & (Bool  "("   "for" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "c"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "a"))) & (Bool (Set (Var "c"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "b")))) "holds"  (Bool (Set (Var "c"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "b4")))  ")" )  ")" )  ")" )))); 
 


























theorem :: LATTICE3:13 (Bool  "for" (Set (Var "V")) "being"   ($#v5_orders_2 :::"antisymmetric"::: )     ($#v1_lattice3 :::"with_suprema"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "u1")) "," (Set (Var "u2")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set (Var "u1"))  ($#k10_lattice3 :::""\/""::: )  (Set (Var "u2")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "u2"))  ($#k10_lattice3 :::""\/""::: )  (Set (Var "u1")))))) ; 
 
theorem :: LATTICE3:14 (Bool  "for" (Set (Var "V")) "being"   ($#v5_orders_2 :::"antisymmetric"::: )     ($#v1_lattice3 :::"with_suprema"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "u1")) "," (Set (Var "u2")) "," (Set (Var "u3")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "V")) "is"   ($#v4_orders_2 :::"transitive"::: )  )) "holds"  (Bool (Set (Set  "(" (Set (Var "u1"))  ($#k10_lattice3 :::""\/""::: )  (Set (Var "u2")) ")" )  ($#k10_lattice3 :::""\/""::: )  (Set (Var "u3")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "u1"))  ($#k10_lattice3 :::""\/""::: )  (Set  "(" (Set (Var "u2"))  ($#k10_lattice3 :::""\/""::: )  (Set (Var "u3")) ")" ))))) ; 
 
theorem :: LATTICE3:15 (Bool  "for" (Set (Var "N")) "being"   ($#v5_orders_2 :::"antisymmetric"::: )     ($#v2_lattice3 :::"with_infima"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "n1")) "," (Set (Var "n2")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) "holds"  (Bool (Set (Set (Var "n1"))  ($#k11_lattice3 :::""/\""::: )  (Set (Var "n2")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n2"))  ($#k11_lattice3 :::""/\""::: )  (Set (Var "n1")))))) ; 
 
theorem :: LATTICE3:16 (Bool  "for" (Set (Var "N")) "being"   ($#v5_orders_2 :::"antisymmetric"::: )     ($#v2_lattice3 :::"with_infima"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N"))  "st" (Bool (Bool (Set (Var "N")) "is"   ($#v4_orders_2 :::"transitive"::: )  )) "holds"  (Bool (Set (Set  "(" (Set (Var "n1"))  ($#k11_lattice3 :::""/\""::: )  (Set (Var "n2")) ")" )  ($#k11_lattice3 :::""/\""::: )  (Set (Var "n3")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n1"))  ($#k11_lattice3 :::""/\""::: )  (Set  "(" (Set (Var "n2"))  ($#k11_lattice3 :::""/\""::: )  (Set (Var "n3")) ")" ))))) ; 
 definitionlet "L" be   ($#v5_orders_2 :::"antisymmetric"::: )     ($#v2_lattice3 :::"with_infima"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; let "x", "y" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); :: original: :::""/\""::: redefine func "x" :::""/\""::: "y" ->   ($#m1_subset_1 :::"Element":::) "of" "L"; commutativity  
(Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")) "holds"  (Bool (Set (Set (Var "x"))  ($#k11_lattice3 :::""/\""::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k11_lattice3 :::""/\""::: )  (Set (Var "x")))))
 ; end; definitionlet "L" be   ($#v5_orders_2 :::"antisymmetric"::: )     ($#v1_lattice3 :::"with_suprema"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; let "x", "y" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); :: original: :::""\/""::: redefine func "x" :::""\/""::: "y" ->   ($#m1_subset_1 :::"Element":::) "of" "L"; commutativity  
(Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")) "holds"  (Bool (Set (Set (Var "x"))  ($#k10_lattice3 :::""\/""::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k10_lattice3 :::""\/""::: )  (Set (Var "x")))))
 ; end; 
theorem :: LATTICE3:17 (Bool  "for" (Set (Var "K")) "being"   ($#v3_orders_2 :::"reflexive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v1_lattice3 :::"with_suprema"::: )     ($#v2_lattice3 :::"with_infima"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "k1")) "," (Set (Var "k2")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds"  (Bool (Set (Set  "(" (Set (Var "k1"))  ($#k12_lattice3 :::""/\""::: )  (Set (Var "k2")) ")" )  ($#k13_lattice3 :::""\/""::: )  (Set (Var "k2")))  ($#r1_hidden :::"="::: )  (Set (Var "k2"))))) ; 
 
theorem :: LATTICE3:18 (Bool  "for" (Set (Var "K")) "being"   ($#v3_orders_2 :::"reflexive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v1_lattice3 :::"with_suprema"::: )     ($#v2_lattice3 :::"with_infima"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "k1")) "," (Set (Var "k2")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds"  (Bool (Set (Set (Var "k1"))  ($#k12_lattice3 :::""/\""::: )  (Set  "(" (Set (Var "k1"))  ($#k13_lattice3 :::""\/""::: )  (Set (Var "k2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "k1"))))) ; 
 
theorem :: LATTICE3:19 (Bool  "for" (Set (Var "A")) "being"   ($#v1_lattice3 :::"with_suprema"::: )     ($#v2_lattice3 :::"with_infima"::: )    ($#l1_orders_2 :::"Poset":::) (Bool  "ex" (Set (Var "L")) "being"   ($#v3_lattices :::"strict"::: )    ($#l3_lattices :::"Lattice":::) "st" (Bool (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "A"))) "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "A"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_lattice3 :::"LattPOSet"::: )  (Set (Var "L")))))) ; 
 definitionlet "A" be    ($#l1_orders_2 :::"RelStr"::: )  ; assume 
(Bool (Set (Const "A")) "is"   ($#v1_lattice3 :::"with_suprema"::: )     ($#v2_lattice3 :::"with_infima"::: )    ($#l1_orders_2 :::"Poset":::))
 ; func  :::"latt"::: "A" ->   ($#v3_lattices :::"strict"::: )    ($#l3_lattices :::"Lattice":::) means :: LATTICE3:def 15 (Bool (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "A") "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "A") "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_lattice3 :::"LattPOSet"::: )  it)); end; 






:: deftheorem    defines :::"latt"::: LATTICE3:def 15 :  (Bool  "for" (Set (Var "A")) "being"    ($#l1_orders_2 :::"RelStr"::: )    "st" (Bool (Bool (Set (Var "A")) "is"   ($#v1_lattice3 :::"with_suprema"::: )     ($#v2_lattice3 :::"with_infima"::: )    ($#l1_orders_2 :::"Poset":::))) "holds"  (Bool  "for" (Set (Var "b2")) "being"   ($#v3_lattices :::"strict"::: )    ($#l3_lattices :::"Lattice":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k14_lattice3 :::"latt"::: )  (Set (Var "A")))) "iff" (Bool (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "A"))) "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "A"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_lattice3 :::"LattPOSet"::: )  (Set (Var "b2"))))  ")" ))); 
 
theorem :: LATTICE3:20 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k2_lattice3 :::"LattRel"::: )  (Set (Var "L")) ")" )  ($#k6_lattice3 :::"~"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k2_lattice3 :::"LattRel"::: )  (Set  "(" (Set (Var "L"))  ($#k1_lattice2 :::".:"::: )  ")" ))) & (Bool (Set (Set  "("  ($#k3_lattice3 :::"LattPOSet"::: )  (Set (Var "L")) ")" )  ($#k7_lattice3 :::"~"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k3_lattice3 :::"LattPOSet"::: )  (Set  "(" (Set (Var "L"))  ($#k1_lattice2 :::".:"::: )  ")" )))  ")" )) ; 
 begin  definitionlet "L" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l3_lattices :::"LattStr"::: )  ; let "p" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); let "X" be    ($#m1_hidden :::"set"::: )  ; pred "p" :::"is_less_than"::: "X" means :: LATTICE3:def 16 (Bool  "for" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" "L"  "st" (Bool (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  "X")) "holds"  (Bool "p"  ($#r1_lattices :::"[="::: )  (Set (Var "q")))); pred "X" :::"is_less_than"::: "p" means :: LATTICE3:def 17 (Bool  "for" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" "L"  "st" (Bool (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  "X")) "holds"  (Bool (Set (Var "q"))  ($#r1_lattices :::"[="::: )  "p")); end; 












:: deftheorem    defines :::"is_less_than"::: LATTICE3:def 16 :  (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l3_lattices :::"LattStr"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "p"))  ($#r3_lattice3 :::"is_less_than"::: )  (Set (Var "X"))) "iff" (Bool  "for" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "p"))  ($#r1_lattices :::"[="::: )  (Set (Var "q"))))  ")" )))); 
 
:: deftheorem    defines :::"is_less_than"::: LATTICE3:def 17 :  (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l3_lattices :::"LattStr"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r4_lattice3 :::"is_less_than"::: )  (Set (Var "p"))) "iff" (Bool  "for" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "q"))  ($#r1_lattices :::"[="::: )  (Set (Var "p"))))  ")" )))); 
 notationlet "L" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l3_lattices :::"LattStr"::: )  ; let "p" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); let "X" be    ($#m1_hidden :::"set"::: )  ; synonym "X" :::"is_greater_than"::: "p" for "p" :::"is_less_than"::: "X"; synonym "p" :::"is_greater_than"::: "X" for "X" :::"is_less_than"::: "p"; end; 
theorem :: LATTICE3:21 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"   (Bool  "("  (Bool (Set (Var "p"))  ($#r3_lattice3 :::"is_less_than"::: )  (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "q")) "," (Set (Var "r")) ($#k7_domain_1 :::"}"::: ) )) "iff" (Bool (Set (Var "p"))  ($#r3_lattices :::"[="::: )  (Set (Set (Var "q"))  ($#k4_lattices :::""/\""::: )  (Set (Var "r"))))  ")" ))) ; 
 
theorem :: LATTICE3:22 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"   (Bool  "("  (Bool (Set (Var "p"))  ($#r4_lattice3 :::"is_greater_than"::: )  (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "q")) "," (Set (Var "r")) ($#k7_domain_1 :::"}"::: ) )) "iff" (Bool (Set (Set (Var "q"))  ($#k3_lattices :::""\/""::: )  (Set (Var "r")))  ($#r3_lattices :::"[="::: )  (Set (Var "p")))  ")" ))) ; 
 definitionlet "IT" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l3_lattices :::"LattStr"::: )  ; attr "IT" is  :::"complete":::  means :: LATTICE3:def 18 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   (Bool  "ex" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT" "st"  (Bool  "("  (Bool (Set (Var "X"))  ($#r4_lattice3 :::"is_less_than"::: )  (Set (Var "p"))) & (Bool  "("   "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT"  "st" (Bool (Bool (Set (Var "X"))  ($#r4_lattice3 :::"is_less_than"::: )  (Set (Var "r")))) "holds"  (Bool (Set (Var "p"))  ($#r1_lattices :::"[="::: )  (Set (Var "r")))  ")" )  ")" ))); attr "IT" is  :::"\/-distributive":::  means :: LATTICE3:def 19 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT"  "st" (Bool (Bool (Set (Var "X"))  ($#r4_lattice3 :::"is_less_than"::: )  (Set (Var "a"))) & (Bool  "("   "for" (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT"  "st" (Bool (Bool (Set (Var "X"))  ($#r4_lattice3 :::"is_less_than"::: )  (Set (Var "d")))) "holds"  (Bool (Set (Var "a"))  ($#r1_lattices :::"[="::: )  (Set (Var "d")))  ")" ) & (Bool  "{"  (Set  "(" (Set (Var "b"))  ($#k2_lattices :::""/\""::: )  (Set (Var "a9")) ")" ) where a9 "is"   ($#m1_subset_1 :::"Element":::) "of" "IT" : (Bool (Set (Var "a9"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  "}"    ($#r4_lattice3 :::"is_less_than"::: )  (Set (Var "c"))) & (Bool  "("   "for" (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT"  "st" (Bool (Bool  "{"  (Set  "(" (Set (Var "b"))  ($#k2_lattices :::""/\""::: )  (Set (Var "a9")) ")" ) where a9 "is"   ($#m1_subset_1 :::"Element":::) "of" "IT" : (Bool (Set (Var "a9"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  "}"    ($#r4_lattice3 :::"is_less_than"::: )  (Set (Var "d")))) "holds"  (Bool (Set (Var "c"))  ($#r1_lattices :::"[="::: )  (Set (Var "d")))  ")" )) "holds"  (Bool (Set (Set (Var "b"))  ($#k2_lattices :::""/\""::: )  (Set (Var "a")))  ($#r1_lattices :::"[="::: )  (Set (Var "c"))))); attr "IT" is  :::"/\-distributive":::  means :: LATTICE3:def 20 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT"  "st" (Bool (Bool (Set (Var "X"))  ($#r3_lattice3 :::"is_greater_than"::: )  (Set (Var "a"))) & (Bool  "("   "for" (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT"  "st" (Bool (Bool (Set (Var "X"))  ($#r3_lattice3 :::"is_greater_than"::: )  (Set (Var "d")))) "holds"  (Bool (Set (Var "d"))  ($#r1_lattices :::"[="::: )  (Set (Var "a")))  ")" ) & (Bool  "{"  (Set  "(" (Set (Var "b"))  ($#k1_lattices :::""\/""::: )  (Set (Var "a9")) ")" ) where a9 "is"   ($#m1_subset_1 :::"Element":::) "of" "IT" : (Bool (Set (Var "a9"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  "}"    ($#r3_lattice3 :::"is_greater_than"::: )  (Set (Var "c"))) & (Bool  "("   "for" (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT"  "st" (Bool (Bool  "{"  (Set  "(" (Set (Var "b"))  ($#k1_lattices :::""\/""::: )  (Set (Var "a9")) ")" ) where a9 "is"   ($#m1_subset_1 :::"Element":::) "of" "IT" : (Bool (Set (Var "a9"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  "}"    ($#r3_lattice3 :::"is_greater_than"::: )  (Set (Var "d")))) "holds"  (Bool (Set (Var "d"))  ($#r1_lattices :::"[="::: )  (Set (Var "c")))  ")" )) "holds"  (Bool (Set (Var "c"))  ($#r1_lattices :::"[="::: )  (Set (Set (Var "b"))  ($#k1_lattices :::""\/""::: )  (Set (Var "a")))))); end; 












:: deftheorem    defines :::"complete"::: LATTICE3:def 18 :  (Bool  "for" (Set (Var "IT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l3_lattices :::"LattStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v4_lattice3 :::"complete"::: )  ) "iff" (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   (Bool  "ex" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st"  (Bool  "("  (Bool (Set (Var "X"))  ($#r4_lattice3 :::"is_less_than"::: )  (Set (Var "p"))) & (Bool  "("   "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT"))  "st" (Bool (Bool (Set (Var "X"))  ($#r4_lattice3 :::"is_less_than"::: )  (Set (Var "r")))) "holds"  (Bool (Set (Var "p"))  ($#r1_lattices :::"[="::: )  (Set (Var "r")))  ")" )  ")" )))  ")" )); 
 
:: deftheorem    defines :::"\/-distributive"::: LATTICE3:def 19 :  (Bool  "for" (Set (Var "IT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l3_lattices :::"LattStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v5_lattice3 :::"\/-distributive"::: )  ) "iff" (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT"))  "st" (Bool (Bool (Set (Var "X"))  ($#r4_lattice3 :::"is_less_than"::: )  (Set (Var "a"))) & (Bool  "("   "for" (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT"))  "st" (Bool (Bool (Set (Var "X"))  ($#r4_lattice3 :::"is_less_than"::: )  (Set (Var "d")))) "holds"  (Bool (Set (Var "a"))  ($#r1_lattices :::"[="::: )  (Set (Var "d")))  ")" ) & (Bool  "{"  (Set  "(" (Set (Var "b"))  ($#k2_lattices :::""/\""::: )  (Set (Var "a9")) ")" ) where a9 "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) : (Bool (Set (Var "a9"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  "}"    ($#r4_lattice3 :::"is_less_than"::: )  (Set (Var "c"))) & (Bool  "("   "for" (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT"))  "st" (Bool (Bool  "{"  (Set  "(" (Set (Var "b"))  ($#k2_lattices :::""/\""::: )  (Set (Var "a9")) ")" ) where a9 "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) : (Bool (Set (Var "a9"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  "}"    ($#r4_lattice3 :::"is_less_than"::: )  (Set (Var "d")))) "holds"  (Bool (Set (Var "c"))  ($#r1_lattices :::"[="::: )  (Set (Var "d")))  ")" )) "holds"  (Bool (Set (Set (Var "b"))  ($#k2_lattices :::""/\""::: )  (Set (Var "a")))  ($#r1_lattices :::"[="::: )  (Set (Var "c")))))  ")" )); 
 
:: deftheorem    defines :::"/\-distributive"::: LATTICE3:def 20 :  (Bool  "for" (Set (Var "IT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l3_lattices :::"LattStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v6_lattice3 :::"/\-distributive"::: )  ) "iff" (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT"))  "st" (Bool (Bool (Set (Var "X"))  ($#r3_lattice3 :::"is_greater_than"::: )  (Set (Var "a"))) & (Bool  "("   "for" (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT"))  "st" (Bool (Bool (Set (Var "X"))  ($#r3_lattice3 :::"is_greater_than"::: )  (Set (Var "d")))) "holds"  (Bool (Set (Var "d"))  ($#r1_lattices :::"[="::: )  (Set (Var "a")))  ")" ) & (Bool  "{"  (Set  "(" (Set (Var "b"))  ($#k1_lattices :::""\/""::: )  (Set (Var "a9")) ")" ) where a9 "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) : (Bool (Set (Var "a9"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  "}"    ($#r3_lattice3 :::"is_greater_than"::: )  (Set (Var "c"))) & (Bool  "("   "for" (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT"))  "st" (Bool (Bool  "{"  (Set  "(" (Set (Var "b"))  ($#k1_lattices :::""\/""::: )  (Set (Var "a9")) ")" ) where a9 "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) : (Bool (Set (Var "a9"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  "}"    ($#r3_lattice3 :::"is_greater_than"::: )  (Set (Var "d")))) "holds"  (Bool (Set (Var "d"))  ($#r1_lattices :::"[="::: )  (Set (Var "c")))  ")" )) "holds"  (Bool (Set (Var "c"))  ($#r1_lattices :::"[="::: )  (Set (Set (Var "b"))  ($#k1_lattices :::""\/""::: )  (Set (Var "a"))))))  ")" )); 
 
theorem :: LATTICE3:23 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "B")) "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r4_lattice3 :::"is_less_than"::: )  (Set (Var "a"))) "iff" (Bool  "{"  (Set  "(" (Set (Var "b"))  ($#k7_lattices :::"`"::: )  ")" ) where b "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "B")) : (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  "}"    ($#r3_lattice3 :::"is_greater_than"::: )  (Set (Set (Var "a"))  ($#k7_lattices :::"`"::: )  ))  ")" )))) ; 
 
theorem :: LATTICE3:24 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "B")) "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r3_lattice3 :::"is_greater_than"::: )  (Set (Var "a"))) "iff" (Bool  "{"  (Set  "(" (Set (Var "b"))  ($#k7_lattices :::"`"::: )  ")" ) where b "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "B")) : (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  "}"    ($#r4_lattice3 :::"is_less_than"::: )  (Set (Set (Var "a"))  ($#k7_lattices :::"`"::: )  ))  ")" )))) ; 
 
theorem :: LATTICE3:25 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_lattice3 :::"BooleLatt"::: )  (Set (Var "X"))) "is"   ($#v4_lattice3 :::"complete"::: )  )) ; 
 registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k1_lattice3 :::"BooleLatt"::: )  "X") ->   ($#v3_lattices :::"strict"::: )     ($#v4_lattice3 :::"complete"::: )   ; 
end; 
theorem :: LATTICE3:26 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_lattice3 :::"BooleLatt"::: )  (Set (Var "X"))) "is"   ($#v5_lattice3 :::"\/-distributive"::: )  )) ; 
 
theorem :: LATTICE3:27 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_lattice3 :::"BooleLatt"::: )  (Set (Var "X"))) "is"   ($#v6_lattice3 :::"/\-distributive"::: )  )) ; 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_lattices :::"strict"::: )     ($#v4_lattices :::"join-commutative"::: )     ($#v5_lattices :::"join-associative"::: )     ($#v6_lattices :::"meet-commutative"::: )     ($#v7_lattices :::"meet-associative"::: )     ($#v8_lattices :::"meet-absorbing"::: )     ($#v9_lattices :::"join-absorbing"::: )     ($#v10_lattices :::"Lattice-like"::: )     ($#v4_lattice3 :::"complete"::: )     ($#v5_lattice3 :::"\/-distributive"::: )     ($#v6_lattice3 :::"/\-distributive"::: )    for    ($#l3_lattices :::"LattStr"::: )  ; 
end; 




theorem :: LATTICE3:28 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"   (Bool  "("  (Bool (Set (Var "p"))  ($#r3_lattice3 :::"is_less_than"::: )  (Set (Var "X"))) "iff" (Bool (Set (Set (Var "p"))  ($#k4_lattice3 :::"%"::: )  )  ($#r1_lattice3 :::"is_<=_than"::: )  (Set (Var "X")))  ")" )))) ; 
 
theorem :: LATTICE3:29 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "p9")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k3_lattice3 :::"LattPOSet"::: )  (Set (Var "L")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "p9"))  ($#r1_lattice3 :::"is_<=_than"::: )  (Set (Var "X"))) "iff" (Bool (Set   ($#k5_lattice3 :::"%"::: )  (Set (Var "p9")))  ($#r3_lattice3 :::"is_less_than"::: )  (Set (Var "X")))  ")" )))) ; 
 
theorem :: LATTICE3:30 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r4_lattice3 :::"is_less_than"::: )  (Set (Var "p"))) "iff" (Bool (Set (Var "X"))  ($#r2_lattice3 :::"is_<=_than"::: )  (Set (Set (Var "p"))  ($#k4_lattice3 :::"%"::: )  ))  ")" )))) ; 
 
theorem :: LATTICE3:31 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "p9")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k3_lattice3 :::"LattPOSet"::: )  (Set (Var "L")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r2_lattice3 :::"is_<=_than"::: )  (Set (Var "p9"))) "iff" (Bool (Set (Var "X"))  ($#r4_lattice3 :::"is_less_than"::: )  (Set   ($#k5_lattice3 :::"%"::: )  (Set (Var "p9"))))  ")" )))) ; 
 registrationlet "A" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_lattice3 :::"complete"::: )    ($#l1_orders_2 :::"Poset":::); 
cluster (Set   ($#k14_lattice3 :::"latt"::: )  "A") ->   ($#v3_lattices :::"strict"::: )     ($#v4_lattice3 :::"complete"::: )   ; 
end; definitionlet "L" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l3_lattices :::"LattStr"::: )  ; assume 
(Bool (Set (Const "L")) "is"   ($#v4_lattice3 :::"complete"::: )    ($#l3_lattices :::"Lattice":::))
 ; let "X" be    ($#m1_hidden :::"set"::: )  ; func  :::""\/"":::  "(" "X" "," "L" ")"  ->   ($#m1_subset_1 :::"Element":::) "of" "L" means :: LATTICE3:def 21 (Bool  "("  (Bool "X"  ($#r4_lattice3 :::"is_less_than"::: )  it) & (Bool  "("   "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Element":::) "of" "L"  "st" (Bool (Bool "X"  ($#r4_lattice3 :::"is_less_than"::: )  (Set (Var "r")))) "holds"  (Bool it  ($#r1_lattices :::"[="::: )  (Set (Var "r")))  ")" )  ")" ); end; 







:: deftheorem    defines :::""\/""::: LATTICE3:def 21 :  (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l3_lattices :::"LattStr"::: )    "st" (Bool (Bool (Set (Var "L")) "is"   ($#v4_lattice3 :::"complete"::: )    ($#l3_lattices :::"Lattice":::))) "holds"  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k15_lattice3 :::""\/""::: )   "(" (Set (Var "X")) "," (Set (Var "L")) ")" )) "iff" (Bool  "("  (Bool (Set (Var "X"))  ($#r4_lattice3 :::"is_less_than"::: )  (Set (Var "b3"))) & (Bool  "("   "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "X"))  ($#r4_lattice3 :::"is_less_than"::: )  (Set (Var "r")))) "holds"  (Bool (Set (Var "b3"))  ($#r1_lattices :::"[="::: )  (Set (Var "r")))  ")" )  ")" )  ")" )))); 
 definitionlet "L" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l3_lattices :::"LattStr"::: )  ; let "X" be    ($#m1_hidden :::"set"::: )  ; func  :::""/\"":::  "(" "X" "," "L" ")"  ->   ($#m1_subset_1 :::"Element":::) "of" "L" equals :: LATTICE3:def 22 (Set   ($#k15_lattice3 :::""\/""::: )   "("  "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Element":::) "of" "L" : (Bool (Set (Var "p"))  ($#r3_lattice3 :::"is_less_than"::: )  "X")  "}"   "," "L" ")" ); end; 






:: deftheorem    defines :::""/\""::: LATTICE3:def 22 :  (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l3_lattices :::"LattStr"::: )    (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k16_lattice3 :::""/\""::: )   "(" (Set (Var "X")) "," (Set (Var "L")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k15_lattice3 :::""\/""::: )   "("  "{"  (Set (Var "p")) where p "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Var "p"))  ($#r3_lattice3 :::"is_less_than"::: )  (Set (Var "X")))  "}"   "," (Set (Var "L")) ")" )))); 
 notationlet "L" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l3_lattices :::"LattStr"::: )  ; let "X" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); synonym  :::""\/""::: "X" for  :::""\/"":::  "(" "X" "," "L" ")" ; synonym  :::""/\""::: "X" for  :::""/\"":::  "(" "X" "," "L" ")" ; end; 















theorem :: LATTICE3:32 (Bool  "for" (Set (Var "C")) "being"   ($#v4_lattice3 :::"complete"::: )    ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k15_lattice3 :::""\/""::: )   "("  "{"  (Set  "(" (Set (Var "a"))  ($#k4_lattices :::""/\""::: )  (Set (Var "b")) ")" ) where b "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C")) : (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  "}"   "," (Set (Var "C")) ")" )  ($#r3_lattices :::"[="::: )  (Set (Set (Var "a"))  ($#k4_lattices :::""/\""::: )  (Set  "("  ($#k15_lattice3 :::""\/""::: )   "(" (Set (Var "X")) "," (Set (Var "C")) ")"  ")" )))))) ; 
 
theorem :: LATTICE3:33 (Bool  "for" (Set (Var "C")) "being"   ($#v4_lattice3 :::"complete"::: )    ($#l3_lattices :::"Lattice":::) "holds"   (Bool  "("  (Bool (Set (Var "C")) "is"   ($#v5_lattice3 :::"\/-distributive"::: )  ) "iff" (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C")) "holds"  (Bool (Set (Set (Var "a"))  ($#k4_lattices :::""/\""::: )  (Set  "("  ($#k15_lattice3 :::""\/""::: )   "(" (Set (Var "X")) "," (Set (Var "C")) ")"  ")" ))  ($#r3_lattices :::"[="::: )  (Set   ($#k15_lattice3 :::""\/""::: )   "("  "{"  (Set  "(" (Set (Var "a"))  ($#k4_lattices :::""/\""::: )  (Set (Var "b")) ")" ) where b "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C")) : (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  "}"   "," (Set (Var "C")) ")" ))))  ")" )) ; 
 
theorem :: LATTICE3:34 (Bool  "for" (Set (Var "C")) "being"   ($#v4_lattice3 :::"complete"::: )    ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k16_lattice3 :::""/\""::: )   "(" (Set (Var "X")) "," (Set (Var "C")) ")" )) "iff" (Bool  "("  (Bool (Set (Var "a"))  ($#r3_lattice3 :::"is_less_than"::: )  (Set (Var "X"))) & (Bool  "("   "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C"))  "st" (Bool (Bool (Set (Var "b"))  ($#r3_lattice3 :::"is_less_than"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "b"))  ($#r3_lattices :::"[="::: )  (Set (Var "a")))  ")" )  ")" )  ")" )))) ; 
 
theorem :: LATTICE3:35 (Bool  "for" (Set (Var "C")) "being"   ($#v4_lattice3 :::"complete"::: )    ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k3_lattices :::""\/""::: )  (Set  "("  ($#k16_lattice3 :::""/\""::: )   "(" (Set (Var "X")) "," (Set (Var "C")) ")"  ")" ))  ($#r3_lattices :::"[="::: )  (Set   ($#k16_lattice3 :::""/\""::: )   "("  "{"  (Set  "(" (Set (Var "a"))  ($#k3_lattices :::""\/""::: )  (Set (Var "b")) ")" ) where b "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C")) : (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  "}"   "," (Set (Var "C")) ")" ))))) ; 
 
theorem :: LATTICE3:36 (Bool  "for" (Set (Var "C")) "being"   ($#v4_lattice3 :::"complete"::: )    ($#l3_lattices :::"Lattice":::) "holds"   (Bool  "("  (Bool (Set (Var "C")) "is"   ($#v6_lattice3 :::"/\-distributive"::: )  ) "iff" (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C")) "holds"  (Bool (Set   ($#k16_lattice3 :::""/\""::: )   "("  "{"  (Set  "(" (Set (Var "a"))  ($#k3_lattices :::""\/""::: )  (Set (Var "b")) ")" ) where b "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C")) : (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  "}"   "," (Set (Var "C")) ")" )  ($#r3_lattices :::"[="::: )  (Set (Set (Var "a"))  ($#k3_lattices :::""\/""::: )  (Set  "("  ($#k16_lattice3 :::""/\""::: )   "(" (Set (Var "X")) "," (Set (Var "C")) ")"  ")" )))))  ")" )) ; 
 
theorem :: LATTICE3:37 (Bool  "for" (Set (Var "C")) "being"   ($#v4_lattice3 :::"complete"::: )    ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k15_lattice3 :::""\/""::: )   "(" (Set (Var "X")) "," (Set (Var "C")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k16_lattice3 :::""/\""::: )   "("  "{"  (Set (Var "a")) where a "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C")) : (Bool (Set (Var "a"))  ($#r4_lattice3 :::"is_greater_than"::: )  (Set (Var "X")))  "}"   "," (Set (Var "C")) ")" )))) ; 
 
theorem :: LATTICE3:38 (Bool  "for" (Set (Var "C")) "being"   ($#v4_lattice3 :::"complete"::: )    ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool  "("  (Bool (Set (Var "a"))  ($#r3_lattices :::"[="::: )  (Set   ($#k15_lattice3 :::""\/""::: )   "(" (Set (Var "X")) "," (Set (Var "C")) ")" )) & (Bool (Set   ($#k16_lattice3 :::""/\""::: )   "(" (Set (Var "X")) "," (Set (Var "C")) ")" )  ($#r3_lattices :::"[="::: )  (Set (Var "a")))  ")" )))) ; 
 
theorem :: LATTICE3:39 (Bool  "for" (Set (Var "C")) "being"   ($#v4_lattice3 :::"complete"::: )    ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r3_lattice3 :::"is_less_than"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "a"))  ($#r3_lattices :::"[="::: )  (Set   ($#k16_lattice3 :::""/\""::: )   "(" (Set (Var "X")) "," (Set (Var "C")) ")" ))))) ; 
 
theorem :: LATTICE3:40 (Bool  "for" (Set (Var "C")) "being"   ($#v4_lattice3 :::"complete"::: )    ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "X"))  ($#r4_lattice3 :::"is_less_than"::: )  (Set (Var "a")))) "holds"  (Bool (Set   ($#k15_lattice3 :::""\/""::: )   "(" (Set (Var "X")) "," (Set (Var "C")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "a")))))) ; 
 
theorem :: LATTICE3:41 (Bool  "for" (Set (Var "C")) "being"   ($#v4_lattice3 :::"complete"::: )    ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C"))  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "a"))  ($#r3_lattice3 :::"is_less_than"::: )  (Set (Var "X")))) "holds"  (Bool (Set   ($#k16_lattice3 :::""/\""::: )   "(" (Set (Var "X")) "," (Set (Var "C")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "a")))))) ; 
 
theorem :: LATTICE3:42 (Bool  "for" (Set (Var "C")) "being"   ($#v4_lattice3 :::"complete"::: )    ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C")) "holds"   (Bool  "("  (Bool (Set   ($#k15_lattice3 :::""\/""::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set   ($#k16_lattice3 :::""/\""::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" ))) ; 
 
theorem :: LATTICE3:43 (Bool  "for" (Set (Var "C")) "being"   ($#v4_lattice3 :::"complete"::: )    ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C")) "holds"   (Bool  "("  (Bool (Set (Set (Var "a"))  ($#k3_lattices :::""\/""::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set   ($#k15_lattice3 :::""\/""::: )  (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k7_domain_1 :::"}"::: ) ))) & (Bool (Set (Set (Var "a"))  ($#k4_lattices :::""/\""::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set   ($#k16_lattice3 :::""/\""::: )  (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k7_domain_1 :::"}"::: ) )))  ")" ))) ; 
 
theorem :: LATTICE3:44 (Bool  "for" (Set (Var "C")) "being"   ($#v4_lattice3 :::"complete"::: )    ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C")) "holds"   (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k15_lattice3 :::""\/""::: )   "("  "{"  (Set (Var "b")) where b "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C")) : (Bool (Set (Var "b"))  ($#r3_lattices :::"[="::: )  (Set (Var "a")))  "}"   "," (Set (Var "C")) ")" )) & (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k16_lattice3 :::""/\""::: )   "("  "{"  (Set (Var "c")) where c "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C")) : (Bool (Set (Var "a"))  ($#r3_lattices :::"[="::: )  (Set (Var "c")))  "}"   "," (Set (Var "C")) ")" ))  ")" ))) ; 
 
theorem :: LATTICE3:45 (Bool  "for" (Set (Var "C")) "being"   ($#v4_lattice3 :::"complete"::: )    ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) "holds"  (Bool  "("  (Bool (Set   ($#k15_lattice3 :::""\/""::: )   "(" (Set (Var "X")) "," (Set (Var "C")) ")" )  ($#r3_lattices :::"[="::: )  (Set   ($#k15_lattice3 :::""\/""::: )   "(" (Set (Var "Y")) "," (Set (Var "C")) ")" )) & (Bool (Set   ($#k16_lattice3 :::""/\""::: )   "(" (Set (Var "Y")) "," (Set (Var "C")) ")" )  ($#r3_lattices :::"[="::: )  (Set   ($#k16_lattice3 :::""/\""::: )   "(" (Set (Var "X")) "," (Set (Var "C")) ")" ))  ")" ))) ; 
 
theorem :: LATTICE3:46 (Bool  "for" (Set (Var "C")) "being"   ($#v4_lattice3 :::"complete"::: )    ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k15_lattice3 :::""\/""::: )   "(" (Set (Var "X")) "," (Set (Var "C")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k15_lattice3 :::""\/""::: )   "("  "{"  (Set (Var "a")) where a "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C")) : (Bool  "ex" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C")) "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r3_lattices :::"[="::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  ")" ))  "}"   "," (Set (Var "C")) ")" )) & (Bool (Set   ($#k16_lattice3 :::""/\""::: )   "(" (Set (Var "X")) "," (Set (Var "C")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k16_lattice3 :::""/\""::: )   "("  "{"  (Set (Var "b")) where b "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C")) : (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C")) "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r3_lattices :::"[="::: )  (Set (Var "b"))) & (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  ")" ))  "}"   "," (Set (Var "C")) ")" ))  ")" ))) ; 
 
theorem :: LATTICE3:47 (Bool  "for" (Set (Var "C")) "being"   ($#v4_lattice3 :::"complete"::: )    ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C"))  "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool  "ex" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C")) "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r3_lattices :::"[="::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))  ")" ))  ")" )) "holds"  (Bool (Set   ($#k15_lattice3 :::""\/""::: )   "(" (Set (Var "X")) "," (Set (Var "C")) ")" )  ($#r3_lattices :::"[="::: )  (Set   ($#k15_lattice3 :::""\/""::: )   "(" (Set (Var "Y")) "," (Set (Var "C")) ")" )))) ; 
 
theorem :: LATTICE3:48 (Bool  "for" (Set (Var "C")) "being"   ($#v4_lattice3 :::"complete"::: )    ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_setfam_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C")))))) "holds"  (Bool (Set   ($#k15_lattice3 :::""\/""::: )   "(" (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "X")) ")" ) "," (Set (Var "C")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k15_lattice3 :::""\/""::: )   "("  "{"  (Set  "("  ($#k15_lattice3 :::""\/""::: )  (Set (Var "Y")) ")" ) where Y "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "C")) : (Bool (Set (Var "Y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  "}"   "," (Set (Var "C")) ")" )))) ; 
 
theorem :: LATTICE3:49 (Bool  "for" (Set (Var "C")) "being"   ($#v4_lattice3 :::"complete"::: )    ($#l3_lattices :::"Lattice":::) "holds"   (Bool  "("  (Bool (Set (Var "C")) "is"   ($#l3_lattices :::"0_Lattice":::)) & (Bool (Set   ($#k5_lattices :::"Bottom"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set   ($#k15_lattice3 :::""\/""::: )   "(" (Set  ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "C")) ")" ))  ")" )) ; 
 
theorem :: LATTICE3:50 (Bool  "for" (Set (Var "C")) "being"   ($#v4_lattice3 :::"complete"::: )    ($#l3_lattices :::"Lattice":::) "holds"   (Bool  "("  (Bool (Set (Var "C")) "is"   ($#l3_lattices :::"1_Lattice":::)) & (Bool (Set   ($#k6_lattices :::"Top"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set   ($#k15_lattice3 :::""\/""::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C"))) "," (Set (Var "C")) ")" ))  ")" )) ; 
 
theorem :: LATTICE3:51 (Bool  "for" (Set (Var "C")) "being"   ($#v4_lattice3 :::"complete"::: )    ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C"))  "st" (Bool (Bool (Set (Var "C")) "is"   ($#l3_lattices :::"I_Lattice":::))) "holds"  (Bool (Set (Set (Var "a"))  ($#k4_filter_0 :::"=>"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set   ($#k15_lattice3 :::""\/""::: )   "("  "{"  (Set (Var "c")) where c "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C")) : (Bool (Set (Set (Var "a"))  ($#k4_lattices :::""/\""::: )  (Set (Var "c")))  ($#r3_lattices :::"[="::: )  (Set (Var "b")))  "}"   "," (Set (Var "C")) ")" )))) ; 
 
theorem :: LATTICE3:52 (Bool  "for" (Set (Var "C")) "being"   ($#v4_lattice3 :::"complete"::: )    ($#l3_lattices :::"Lattice":::)  "st" (Bool (Bool (Set (Var "C")) "is"   ($#l3_lattices :::"I_Lattice":::))) "holds"  (Bool (Set (Var "C")) "is"   ($#v5_lattice3 :::"\/-distributive"::: )  )) ; 
 
theorem :: LATTICE3:53 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "D")) "being"   ($#v4_lattice3 :::"complete"::: )     ($#v5_lattice3 :::"\/-distributive"::: )    ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "D")) "holds"   (Bool  "("  (Bool (Set (Set (Var "a"))  ($#k4_lattices :::""/\""::: )  (Set  "("  ($#k15_lattice3 :::""\/""::: )   "(" (Set (Var "X")) "," (Set (Var "D")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k15_lattice3 :::""\/""::: )   "("  "{"  (Set  "(" (Set (Var "a"))  ($#k4_lattices :::""/\""::: )  (Set (Var "b1")) ")" ) where b1 "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "D")) : (Bool (Set (Var "b1"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  "}"   "," (Set (Var "D")) ")" )) & (Bool (Set (Set  "("  ($#k15_lattice3 :::""\/""::: )   "(" (Set (Var "X")) "," (Set (Var "D")) ")"  ")" )  ($#k4_lattices :::""/\""::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k15_lattice3 :::""\/""::: )   "("  "{"  (Set  "(" (Set (Var "b2"))  ($#k4_lattices :::""/\""::: )  (Set (Var "a")) ")" ) where b2 "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "D")) : (Bool (Set (Var "b2"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  "}"   "," (Set (Var "D")) ")" ))  ")" )))) ; 
 
theorem :: LATTICE3:54 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "D")) "being"   ($#v4_lattice3 :::"complete"::: )     ($#v6_lattice3 :::"/\-distributive"::: )    ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "D")) "holds"   (Bool  "("  (Bool (Set (Set (Var "a"))  ($#k3_lattices :::""\/""::: )  (Set  "("  ($#k16_lattice3 :::""/\""::: )   "(" (Set (Var "X")) "," (Set (Var "D")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k16_lattice3 :::""/\""::: )   "("  "{"  (Set  "(" (Set (Var "a"))  ($#k3_lattices :::""\/""::: )  (Set (Var "b1")) ")" ) where b1 "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "D")) : (Bool (Set (Var "b1"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  "}"   "," (Set (Var "D")) ")" )) & (Bool (Set (Set  "("  ($#k16_lattice3 :::""/\""::: )   "(" (Set (Var "X")) "," (Set (Var "D")) ")"  ")" )  ($#k3_lattices :::""\/""::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k16_lattice3 :::""/\""::: )   "("  "{"  (Set  "(" (Set (Var "b2"))  ($#k3_lattices :::""\/""::: )  (Set (Var "a")) ")" ) where b2 "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "D")) : (Bool (Set (Var "b2"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  "}"   "," (Set (Var "D")) ")" ))  ")" )))) ; 
 scheme  :: LATTICE3:sch 1 SingleFraenkel{ F1() ->    ($#m1_hidden :::"set"::: )  , F2() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "{"  (Set F1 "("  ")" ) where a "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" ) : (Bool P1[(Set (Var "a"))])  "}"    ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set F1 "("  ")" ) ($#k1_tarski :::"}"::: ) ))
 provided
(Bool  "ex" (Set (Var "a")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" ) "st" (Bool P1[(Set (Var "a"))]))
 proof 


end; scheme  :: LATTICE3:sch 2 FuncFraenkel{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , 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 F2 "("  ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set F4 "("  ")" )))
 proof 


end; 
theorem :: LATTICE3:55 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k9_setfam_1 :::"bool"::: )  (Set (Var "D")) ")" ) "," (Set (Var "D"))  "st" (Bool (Bool  "("   "for" (Set (Var "a")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "D")) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" ) & (Bool  "("   "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "D")) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k5_setfam_1 :::"union"::: )  (Set (Var "X")) ")" )))  ")" )) "holds"  (Bool  "ex" (Set (Var "L")) "being"   ($#v3_lattices :::"strict"::: )     ($#v4_lattice3 :::"complete"::: )    ($#l3_lattices :::"Lattice":::) "st"  (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set (Var "D"))) & (Bool  "("   "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds"  (Bool (Set   ($#k15_lattice3 :::""\/""::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "X"))))  ")" )  ")" )))) ;