:: BOOLEALG  semantic presentation begin  








definitionlet "L" be   ($#l3_lattices :::"Lattice":::); let "X", "Y" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); func "X" :::"\"::: "Y" ->   ($#m1_subset_1 :::"Element":::) "of" "L" equals :: BOOLEALG:def 1 (Set "X"  ($#k4_lattices :::""/\""::: )  (Set  "(" "Y"  ($#k7_lattices :::"`"::: )  ")" )); end; 







:: deftheorem    defines :::"\"::: BOOLEALG:def 1 :  (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k4_lattices :::""/\""::: )  (Set  "(" (Set (Var "Y"))  ($#k7_lattices :::"`"::: )  ")" ))))); 
 definitionlet "L" be   ($#l3_lattices :::"Lattice":::); let "X", "Y" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); func "X" :::"\+\"::: "Y" ->   ($#m1_subset_1 :::"Element":::) "of" "L" equals :: BOOLEALG:def 2 (Set (Set  "(" "X"  ($#k1_boolealg :::"\"::: )  "Y" ")" )  ($#k3_lattices :::""\/""::: )  (Set  "(" "Y"  ($#k1_boolealg :::"\"::: )  "X" ")" )); end; 







:: deftheorem    defines :::"\+\"::: BOOLEALG:def 2 :  (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "X"))  ($#k2_boolealg :::"\+\"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set (Var "Y")) ")" )  ($#k3_lattices :::""\/""::: )  (Set  "(" (Set (Var "Y"))  ($#k1_boolealg :::"\"::: )  (Set (Var "X")) ")" ))))); 
 definitionlet "L" be   ($#l3_lattices :::"Lattice":::); let "X", "Y" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); :: original: :::"="::: redefine pred "X" :::"="::: "Y" means :: BOOLEALG:def 3 (Bool  "("  (Bool "X"  ($#r3_lattices :::"[="::: )  "Y") & (Bool "Y"  ($#r3_lattices :::"[="::: )  "X")  ")" ); end; 






:: deftheorem    defines :::"="::: BOOLEALG:def 3 :  (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r1_boolealg :::"="::: )  (Set (Var "Y"))) "iff" (Bool  "("  (Bool (Set (Var "X"))  ($#r3_lattices :::"[="::: )  (Set (Var "Y"))) & (Bool (Set (Var "Y"))  ($#r3_lattices :::"[="::: )  (Set (Var "X")))  ")" )  ")" ))); 
 definitionlet "L" be   ($#l3_lattices :::"Lattice":::); let "X", "Y" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); pred "X" :::"meets"::: "Y" means :: BOOLEALG:def 4 (Bool (Set "X"  ($#k4_lattices :::""/\""::: )  "Y")  ($#r1_hidden :::"<>"::: )  (Set   ($#k5_lattices :::"Bottom"::: )  "L")); end; 






:: deftheorem    defines :::"meets"::: BOOLEALG:def 4 :  (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r2_boolealg :::"meets"::: )  (Set (Var "Y"))) "iff" (Bool (Set (Set (Var "X"))  ($#k4_lattices :::""/\""::: )  (Set (Var "Y")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k5_lattices :::"Bottom"::: )  (Set (Var "L"))))  ")" ))); 
 notationlet "L" be   ($#l3_lattices :::"Lattice":::); let "X", "Y" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); antonym "X" :::"misses"::: "Y" for "X" :::"meets"::: "Y"; end; 
theorem :: BOOLEALG:1 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Set (Var "X"))  ($#k3_lattices :::""\/""::: )  (Set (Var "Y")))  ($#r3_lattices :::"[="::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Var "X"))  ($#r3_lattices :::"[="::: )  (Set (Var "Z"))))) ; 
 
theorem :: BOOLEALG:2 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "X"))  ($#k4_lattices :::""/\""::: )  (Set (Var "Y")))  ($#r3_lattices :::"[="::: )  (Set (Set (Var "X"))  ($#k3_lattices :::""\/""::: )  (Set (Var "Z")))))) ; 
 
theorem :: BOOLEALG:3 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Z")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "X"))  ($#r3_lattices :::"[="::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set (Var "Y")))  ($#r3_lattices :::"[="::: )  (Set (Var "Z"))))) ; 
 
theorem :: BOOLEALG:4 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set (Var "Y")))  ($#r3_lattices :::"[="::: )  (Set (Var "Z"))) & (Bool (Set (Set (Var "Y"))  ($#k1_boolealg :::"\"::: )  (Set (Var "X")))  ($#r3_lattices :::"[="::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set (Var "X"))  ($#k2_boolealg :::"\+\"::: )  (Set (Var "Y")))  ($#r3_lattices :::"[="::: )  (Set (Var "Z"))))) ; 
 
theorem :: BOOLEALG:5 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r1_boolealg :::"="::: )  (Set (Set (Var "Y"))  ($#k3_lattices :::""\/""::: )  (Set (Var "Z")))) "iff" (Bool  "("  (Bool (Set (Var "Y"))  ($#r3_lattices :::"[="::: )  (Set (Var "X"))) & (Bool (Set (Var "Z"))  ($#r3_lattices :::"[="::: )  (Set (Var "X"))) & (Bool  "("   "for" (Set (Var "V")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "Y"))  ($#r3_lattices :::"[="::: )  (Set (Var "V"))) & (Bool (Set (Var "Z"))  ($#r3_lattices :::"[="::: )  (Set (Var "V")))) "holds"  (Bool (Set (Var "X"))  ($#r3_lattices :::"[="::: )  (Set (Var "V")))  ")" )  ")" )  ")" ))) ; 
 
theorem :: BOOLEALG:6 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r1_boolealg :::"="::: )  (Set (Set (Var "Y"))  ($#k4_lattices :::""/\""::: )  (Set (Var "Z")))) "iff" (Bool  "("  (Bool (Set (Var "X"))  ($#r3_lattices :::"[="::: )  (Set (Var "Y"))) & (Bool (Set (Var "X"))  ($#r3_lattices :::"[="::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "V")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "V"))  ($#r3_lattices :::"[="::: )  (Set (Var "Y"))) & (Bool (Set (Var "V"))  ($#r3_lattices :::"[="::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Var "V"))  ($#r3_lattices :::"[="::: )  (Set (Var "X")))  ")" )  ")" )  ")" ))) ; 
 
theorem :: BOOLEALG:7 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r2_boolealg :::"meets"::: )  (Set (Var "X"))) "iff" (Bool (Set (Var "X"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k5_lattices :::"Bottom"::: )  (Set (Var "L"))))  ")" ))) ; 
 definitionlet "L" be   ($#l3_lattices :::"Lattice":::); let "X", "Y" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); :: original: :::"meets"::: redefine pred "X" :::"meets"::: "Y"; symmetry  
(Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L"))  "st" (Bool (Bool ((Set (Const "L")) "," (Set (Var "b1")) "," (Set (Var "b2"))))) "holds"  (Bool ((Set (Const "L")) "," (Set (Var "b2")) "," (Set (Var "b1")))))
 ; :: 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"))  ($#k2_boolealg :::"\+\"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "Y"))  ($#k2_boolealg :::"\+\"::: )  (Set (Var "X")))))
 ; :: original: :::"meets"::: redefine pred "X" :::"misses"::: "Y"; symmetry  
(Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L"))  "st" (Bool (Bool ((Set (Const "L")) "," (Set (Var "b1")) "," (Set (Var "b2"))))) "holds"  (Bool  "not" (Bool ((Set (Const "L")) "," (Set (Var "b2")) "," (Set (Var "b1"))))))
 ; end; begin  begin  








theorem :: BOOLEALG:8 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"D_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Set  "(" (Set (Var "X"))  ($#k4_lattices :::""/\""::: )  (Set (Var "Y")) ")" )  ($#k3_lattices :::""\/""::: )  (Set  "(" (Set (Var "X"))  ($#k4_lattices :::""/\""::: )  (Set (Var "Z")) ")" ))  ($#r1_boolealg :::"="::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "X"))  ($#r3_lattices :::"[="::: )  (Set (Set (Var "Y"))  ($#k3_lattices :::""\/""::: )  (Set (Var "Z")))))) ; 
 begin  








theorem :: BOOLEALG:9 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"0_Lattice":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "X"))  ($#r3_lattices :::"[="::: )  (Set   ($#k5_lattices :::"Bottom"::: )  (Set (Var "L"))))) "holds"  (Bool (Set (Var "X"))  ($#r1_boolealg :::"="::: )  (Set   ($#k5_lattices :::"Bottom"::: )  (Set (Var "L")))))) ; 
 
theorem :: BOOLEALG:10 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"0_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "X"))  ($#r3_lattices :::"[="::: )  (Set (Var "Y"))) & (Bool (Set (Var "X"))  ($#r3_lattices :::"[="::: )  (Set (Var "Z"))) & (Bool (Set (Set (Var "Y"))  ($#k4_lattices :::""/\""::: )  (Set (Var "Z")))  ($#r1_boolealg :::"="::: )  (Set   ($#k5_lattices :::"Bottom"::: )  (Set (Var "L"))))) "holds"  (Bool (Set (Var "X"))  ($#r1_boolealg :::"="::: )  (Set   ($#k5_lattices :::"Bottom"::: )  (Set (Var "L")))))) ; 
 
theorem :: BOOLEALG:11 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"0_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"   (Bool  "("  (Bool (Set (Set (Var "X"))  ($#k3_lattices :::""\/""::: )  (Set (Var "Y")))  ($#r1_boolealg :::"="::: )  (Set   ($#k5_lattices :::"Bottom"::: )  (Set (Var "L")))) "iff" (Bool  "("  (Bool (Set (Var "X"))  ($#r1_boolealg :::"="::: )  (Set   ($#k5_lattices :::"Bottom"::: )  (Set (Var "L")))) & (Bool (Set (Var "Y"))  ($#r1_boolealg :::"="::: )  (Set   ($#k5_lattices :::"Bottom"::: )  (Set (Var "L"))))  ")" )  ")" ))) ; 
 
theorem :: BOOLEALG:12 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"0_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "X"))  ($#r3_lattices :::"[="::: )  (Set (Var "Y"))) & (Bool (Set (Set (Var "Y"))  ($#k4_lattices :::""/\""::: )  (Set (Var "Z")))  ($#r1_boolealg :::"="::: )  (Set   ($#k5_lattices :::"Bottom"::: )  (Set (Var "L"))))) "holds"  (Bool (Set (Set (Var "X"))  ($#k4_lattices :::""/\""::: )  (Set (Var "Z")))  ($#r1_boolealg :::"="::: )  (Set   ($#k5_lattices :::"Bottom"::: )  (Set (Var "L")))))) ; 
 
theorem :: BOOLEALG:13 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"0_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "X"))  ($#r3_boolealg :::"meets"::: )  (Set (Var "Y"))) & (Bool (Set (Var "Y"))  ($#r3_lattices :::"[="::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Var "X"))  ($#r3_boolealg :::"meets"::: )  (Set (Var "Z"))))) ; 
 
theorem :: BOOLEALG:14 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"0_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "X"))  ($#r3_boolealg :::"meets"::: )  (Set (Set (Var "Y"))  ($#k4_lattices :::""/\""::: )  (Set (Var "Z"))))) "holds"  (Bool  "("  (Bool (Set (Var "X"))  ($#r3_boolealg :::"meets"::: )  (Set (Var "Y"))) & (Bool (Set (Var "X"))  ($#r3_boolealg :::"meets"::: )  (Set (Var "Z")))  ")" ))) ; 
 
theorem :: BOOLEALG:15 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"0_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "X"))  ($#r3_boolealg :::"meets"::: )  (Set (Set (Var "Y"))  ($#k1_boolealg :::"\"::: )  (Set (Var "Z"))))) "holds"  (Bool (Set (Var "X"))  ($#r3_boolealg :::"meets"::: )  (Set (Var "Y"))))) ; 
 
theorem :: BOOLEALG:16 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"0_Lattice":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "holds" (Bool (Set (Var "X"))  ($#r4_boolealg :::"misses"::: )  (Set   ($#k5_lattices :::"Bottom"::: )  (Set (Var "L")))))) ; 
 
theorem :: BOOLEALG:17 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"0_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Z")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "X"))  ($#r4_boolealg :::"misses"::: )  (Set (Var "Z"))) & (Bool (Set (Var "Y"))  ($#r3_lattices :::"[="::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Var "X"))  ($#r4_boolealg :::"misses"::: )  (Set (Var "Y"))))) ; 
 
theorem :: BOOLEALG:18 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"0_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool  "("  (Bool (Set (Var "X"))  ($#r4_boolealg :::"misses"::: )  (Set (Var "Y"))) "or" (Bool (Set (Var "X"))  ($#r4_boolealg :::"misses"::: )  (Set (Var "Z")))  ")" )) "holds"  (Bool (Set (Var "X"))  ($#r4_boolealg :::"misses"::: )  (Set (Set (Var "Y"))  ($#k4_lattices :::""/\""::: )  (Set (Var "Z")))))) ; 
 
theorem :: BOOLEALG:19 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"0_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "X"))  ($#r3_lattices :::"[="::: )  (Set (Var "Y"))) & (Bool (Set (Var "X"))  ($#r3_lattices :::"[="::: )  (Set (Var "Z"))) & (Bool (Set (Var "Y"))  ($#r4_boolealg :::"misses"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Var "X"))  ($#r1_boolealg :::"="::: )  (Set   ($#k5_lattices :::"Bottom"::: )  (Set (Var "L")))))) ; 
 
theorem :: BOOLEALG:20 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"0_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "X"))  ($#r4_boolealg :::"misses"::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Set (Var "Z"))  ($#k4_lattices :::""/\""::: )  (Set (Var "X")))  ($#r4_boolealg :::"misses"::: )  (Set (Set (Var "Z"))  ($#k4_lattices :::""/\""::: )  (Set (Var "Y")))))) ; 
 begin  









theorem :: BOOLEALG:21 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set (Var "Y")))  ($#r3_lattices :::"[="::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Var "X"))  ($#r3_lattices :::"[="::: )  (Set (Set (Var "Y"))  ($#k3_lattices :::""\/""::: )  (Set (Var "Z")))))) ; 
 
theorem :: BOOLEALG:22 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "X"))  ($#r3_lattices :::"[="::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Set (Var "Z"))  ($#k1_boolealg :::"\"::: )  (Set (Var "Y")))  ($#r3_lattices :::"[="::: )  (Set (Set (Var "Z"))  ($#k1_boolealg :::"\"::: )  (Set (Var "X")))))) ; 
 
theorem :: BOOLEALG:23 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "V")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "X"))  ($#r3_lattices :::"[="::: )  (Set (Var "Y"))) & (Bool (Set (Var "Z"))  ($#r3_lattices :::"[="::: )  (Set (Var "V")))) "holds"  (Bool (Set (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set (Var "V")))  ($#r3_lattices :::"[="::: )  (Set (Set (Var "Y"))  ($#k1_boolealg :::"\"::: )  (Set (Var "Z")))))) ; 
 
theorem :: BOOLEALG:24 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "X"))  ($#r3_lattices :::"[="::: )  (Set (Set (Var "Y"))  ($#k3_lattices :::""\/""::: )  (Set (Var "Z"))))) "holds"  (Bool (Set (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set (Var "Y")))  ($#r3_lattices :::"[="::: )  (Set (Var "Z"))))) ; 
 
theorem :: BOOLEALG:25 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "X"))  ($#k7_lattices :::"`"::: )  )  ($#r3_lattices :::"[="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k4_lattices :::""/\""::: )  (Set (Var "Y")) ")" )  ($#k7_lattices :::"`"::: )  )))) ; 
 
theorem :: BOOLEALG:26 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "X"))  ($#k3_lattices :::""\/""::: )  (Set (Var "Y")) ")" )  ($#k7_lattices :::"`"::: )  )  ($#r3_lattices :::"[="::: )  (Set (Set (Var "X"))  ($#k7_lattices :::"`"::: )  )))) ; 
 
theorem :: BOOLEALG:27 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "X"))  ($#r3_lattices :::"[="::: )  (Set (Set (Var "Y"))  ($#k1_boolealg :::"\"::: )  (Set (Var "X"))))) "holds"  (Bool (Set (Var "X"))  ($#r1_boolealg :::"="::: )  (Set   ($#k5_lattices :::"Bottom"::: )  (Set (Var "L")))))) ; 
 
theorem :: BOOLEALG:28 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "X"))  ($#r3_lattices :::"[="::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Var "Y"))  ($#r1_boolealg :::"="::: )  (Set (Set (Var "X"))  ($#k3_lattices :::""\/""::: )  (Set  "(" (Set (Var "Y"))  ($#k1_boolealg :::"\"::: )  (Set (Var "X")) ")" ))))) ; 
 
theorem :: BOOLEALG:29 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"   (Bool  "("  (Bool (Set (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set (Var "Y")))  ($#r1_boolealg :::"="::: )  (Set   ($#k5_lattices :::"Bottom"::: )  (Set (Var "L")))) "iff" (Bool (Set (Var "X"))  ($#r3_lattices :::"[="::: )  (Set (Var "Y")))  ")" ))) ; 
 
theorem :: BOOLEALG:30 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "X"))  ($#r3_lattices :::"[="::: )  (Set (Set (Var "Y"))  ($#k3_lattices :::""\/""::: )  (Set (Var "Z")))) & (Bool (Set (Set (Var "X"))  ($#k4_lattices :::""/\""::: )  (Set (Var "Z")))  ($#r1_boolealg :::"="::: )  (Set   ($#k5_lattices :::"Bottom"::: )  (Set (Var "L"))))) "holds"  (Bool (Set (Var "X"))  ($#r3_lattices :::"[="::: )  (Set (Var "Y"))))) ; 
 
theorem :: BOOLEALG:31 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "X"))  ($#k3_lattices :::""\/""::: )  (Set (Var "Y")))  ($#r1_boolealg :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set (Var "Y")) ")" )  ($#k3_lattices :::""\/""::: )  (Set (Var "Y")))))) ; 
 
theorem :: BOOLEALG:32 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set  "(" (Set (Var "X"))  ($#k3_lattices :::""\/""::: )  (Set (Var "Y")) ")" ))  ($#r1_boolealg :::"="::: )  (Set   ($#k5_lattices :::"Bottom"::: )  (Set (Var "L")))))) ; 
 
theorem :: BOOLEALG:33 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set  "(" (Set (Var "X"))  ($#k4_lattices :::""/\""::: )  (Set (Var "Y")) ")" ))  ($#r1_boolealg :::"="::: )  (Set (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BOOLEALG:34 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set (Var "Y")) ")" )  ($#k4_lattices :::""/\""::: )  (Set (Var "Y")))  ($#r1_boolealg :::"="::: )  (Set   ($#k5_lattices :::"Bottom"::: )  (Set (Var "L")))))) ; 
 
theorem :: BOOLEALG:35 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "X"))  ($#k3_lattices :::""\/""::: )  (Set  "(" (Set (Var "Y"))  ($#k1_boolealg :::"\"::: )  (Set (Var "X")) ")" ))  ($#r1_boolealg :::"="::: )  (Set (Set (Var "X"))  ($#k3_lattices :::""\/""::: )  (Set (Var "Y")))))) ; 
 
theorem :: BOOLEALG:36 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "X"))  ($#k4_lattices :::""/\""::: )  (Set (Var "Y")) ")" )  ($#k3_lattices :::""\/""::: )  (Set  "(" (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set (Var "Y")) ")" ))  ($#r1_boolealg :::"="::: )  (Set (Var "X"))))) ; 
 
theorem :: BOOLEALG:37 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set  "(" (Set (Var "Y"))  ($#k1_boolealg :::"\"::: )  (Set (Var "Z")) ")" ))  ($#r1_boolealg :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set (Var "Y")) ")" )  ($#k3_lattices :::""\/""::: )  (Set  "(" (Set (Var "X"))  ($#k4_lattices :::""/\""::: )  (Set (Var "Z")) ")" ))))) ; 
 
theorem :: BOOLEALG:38 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set  "(" (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set (Var "Y")) ")" ))  ($#r1_boolealg :::"="::: )  (Set (Set (Var "X"))  ($#k4_lattices :::""/\""::: )  (Set (Var "Y")))))) ; 
 
theorem :: BOOLEALG:39 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "X"))  ($#k3_lattices :::""\/""::: )  (Set (Var "Y")) ")" )  ($#k1_boolealg :::"\"::: )  (Set (Var "Y")))  ($#r1_boolealg :::"="::: )  (Set (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BOOLEALG:40 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"   (Bool  "("  (Bool (Set (Set (Var "X"))  ($#k4_lattices :::""/\""::: )  (Set (Var "Y")))  ($#r1_boolealg :::"="::: )  (Set   ($#k5_lattices :::"Bottom"::: )  (Set (Var "L")))) "iff" (Bool (Set (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set (Var "Y")))  ($#r1_boolealg :::"="::: )  (Set (Var "X")))  ")" ))) ; 
 
theorem :: BOOLEALG:41 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set  "(" (Set (Var "Y"))  ($#k3_lattices :::""\/""::: )  (Set (Var "Z")) ")" ))  ($#r1_boolealg :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set (Var "Y")) ")" )  ($#k4_lattices :::""/\""::: )  (Set  "(" (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set (Var "Z")) ")" ))))) ; 
 
theorem :: BOOLEALG:42 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set  "(" (Set (Var "Y"))  ($#k4_lattices :::""/\""::: )  (Set (Var "Z")) ")" ))  ($#r1_boolealg :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set (Var "Y")) ")" )  ($#k3_lattices :::""\/""::: )  (Set  "(" (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set (Var "Z")) ")" ))))) ; 
 
theorem :: BOOLEALG:43 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "X"))  ($#k4_lattices :::""/\""::: )  (Set  "(" (Set (Var "Y"))  ($#k1_boolealg :::"\"::: )  (Set (Var "Z")) ")" ))  ($#r1_boolealg :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k4_lattices :::""/\""::: )  (Set (Var "Y")) ")" )  ($#k1_boolealg :::"\"::: )  (Set  "(" (Set (Var "X"))  ($#k4_lattices :::""/\""::: )  (Set (Var "Z")) ")" ))))) ; 
 
theorem :: BOOLEALG:44 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "X"))  ($#k3_lattices :::""\/""::: )  (Set (Var "Y")) ")" )  ($#k1_boolealg :::"\"::: )  (Set  "(" (Set (Var "X"))  ($#k4_lattices :::""/\""::: )  (Set (Var "Y")) ")" ))  ($#r1_boolealg :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set (Var "Y")) ")" )  ($#k3_lattices :::""\/""::: )  (Set  "(" (Set (Var "Y"))  ($#k1_boolealg :::"\"::: )  (Set (Var "X")) ")" ))))) ; 
 
theorem :: BOOLEALG:45 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set (Var "Y")) ")" )  ($#k1_boolealg :::"\"::: )  (Set (Var "Z")))  ($#r1_boolealg :::"="::: )  (Set (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set  "(" (Set (Var "Y"))  ($#k3_lattices :::""\/""::: )  (Set (Var "Z")) ")" ))))) ; 
 
theorem :: BOOLEALG:46 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set (Var "Y")))  ($#r1_boolealg :::"="::: )  (Set (Set (Var "Y"))  ($#k1_boolealg :::"\"::: )  (Set (Var "X"))))) "holds"  (Bool (Set (Var "X"))  ($#r1_boolealg :::"="::: )  (Set (Var "Y"))))) ; 
 
theorem :: BOOLEALG:47 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set  "("  ($#k5_lattices :::"Bottom"::: )  (Set (Var "L")) ")" ))  ($#r1_boolealg :::"="::: )  (Set (Var "X"))))) ; 
 
theorem :: BOOLEALG:48 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set (Var "Y")) ")" )  ($#k7_lattices :::"`"::: )  )  ($#r1_boolealg :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k7_lattices :::"`"::: )  ")" )  ($#k3_lattices :::""\/""::: )  (Set (Var "Y")))))) ; 
 
theorem :: BOOLEALG:49 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r3_boolealg :::"meets"::: )  (Set (Set (Var "Y"))  ($#k3_lattices :::""\/""::: )  (Set (Var "Z")))) "iff" (Bool  "("  (Bool (Set (Var "X"))  ($#r3_boolealg :::"meets"::: )  (Set (Var "Y"))) "or" (Bool (Set (Var "X"))  ($#r3_boolealg :::"meets"::: )  (Set (Var "Z")))  ")" )  ")" ))) ; 
 
theorem :: BOOLEALG:50 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "holds" (Bool (Set (Set (Var "X"))  ($#k4_lattices :::""/\""::: )  (Set (Var "Y")))  ($#r4_boolealg :::"misses"::: )  (Set (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BOOLEALG:51 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r4_boolealg :::"misses"::: )  (Set (Set (Var "Y"))  ($#k3_lattices :::""\/""::: )  (Set (Var "Z")))) "iff" (Bool  "("  (Bool (Set (Var "X"))  ($#r4_boolealg :::"misses"::: )  (Set (Var "Y"))) & (Bool (Set (Var "X"))  ($#r4_boolealg :::"misses"::: )  (Set (Var "Z")))  ")" )  ")" ))) ; 
 
theorem :: BOOLEALG:52 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "holds" (Bool (Set (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set (Var "Y")))  ($#r4_boolealg :::"misses"::: )  (Set (Var "Y"))))) ; 
 
theorem :: BOOLEALG:53 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "X"))  ($#r4_boolealg :::"misses"::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Set  "(" (Set (Var "X"))  ($#k3_lattices :::""\/""::: )  (Set (Var "Y")) ")" )  ($#k1_boolealg :::"\"::: )  (Set (Var "Y")))  ($#r1_boolealg :::"="::: )  (Set (Var "X"))))) ; 
 
theorem :: BOOLEALG:54 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Set  "(" (Set (Var "X"))  ($#k7_lattices :::"`"::: )  ")" )  ($#k3_lattices :::""\/""::: )  (Set  "(" (Set (Var "Y"))  ($#k7_lattices :::"`"::: )  ")" ))  ($#r1_boolealg :::"="::: )  (Set (Set (Var "X"))  ($#k3_lattices :::""\/""::: )  (Set (Var "Y")))) & (Bool (Set (Var "X"))  ($#r4_boolealg :::"misses"::: )  (Set (Set (Var "X"))  ($#k7_lattices :::"`"::: )  )) & (Bool (Set (Var "Y"))  ($#r4_boolealg :::"misses"::: )  (Set (Set (Var "Y"))  ($#k7_lattices :::"`"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Var "X"))  ($#r1_boolealg :::"="::: )  (Set (Set (Var "Y"))  ($#k7_lattices :::"`"::: )  )) & (Bool (Set (Var "Y"))  ($#r1_boolealg :::"="::: )  (Set (Set (Var "X"))  ($#k7_lattices :::"`"::: )  ))  ")" ))) ; 
 
theorem :: BOOLEALG:55 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Set  "(" (Set (Var "X"))  ($#k7_lattices :::"`"::: )  ")" )  ($#k3_lattices :::""\/""::: )  (Set  "(" (Set (Var "Y"))  ($#k7_lattices :::"`"::: )  ")" ))  ($#r1_boolealg :::"="::: )  (Set (Set (Var "X"))  ($#k3_lattices :::""\/""::: )  (Set (Var "Y")))) & (Bool (Set (Var "Y"))  ($#r4_boolealg :::"misses"::: )  (Set (Set (Var "X"))  ($#k7_lattices :::"`"::: )  )) & (Bool (Set (Var "X"))  ($#r4_boolealg :::"misses"::: )  (Set (Set (Var "Y"))  ($#k7_lattices :::"`"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Var "X"))  ($#r1_boolealg :::"="::: )  (Set (Set (Var "X"))  ($#k7_lattices :::"`"::: )  )) & (Bool (Set (Var "Y"))  ($#r1_boolealg :::"="::: )  (Set (Set (Var "Y"))  ($#k7_lattices :::"`"::: )  ))  ")" ))) ; 
 
theorem :: BOOLEALG:56 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "X"))  ($#k3_boolealg :::"\+\"::: )  (Set  "("  ($#k5_lattices :::"Bottom"::: )  (Set (Var "L")) ")" ))  ($#r1_boolealg :::"="::: )  (Set (Var "X"))))) ; 
 
theorem :: BOOLEALG:57 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "X"))  ($#k3_boolealg :::"\+\"::: )  (Set (Var "X")))  ($#r1_boolealg :::"="::: )  (Set   ($#k5_lattices :::"Bottom"::: )  (Set (Var "L")))))) ; 
 
theorem :: BOOLEALG:58 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "holds" (Bool (Set (Set (Var "X"))  ($#k4_lattices :::""/\""::: )  (Set (Var "Y")))  ($#r4_boolealg :::"misses"::: )  (Set (Set (Var "X"))  ($#k3_boolealg :::"\+\"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BOOLEALG:59 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "X"))  ($#k3_lattices :::""\/""::: )  (Set (Var "Y")))  ($#r1_boolealg :::"="::: )  (Set (Set (Var "X"))  ($#k3_boolealg :::"\+\"::: )  (Set  "(" (Set (Var "Y"))  ($#k1_boolealg :::"\"::: )  (Set (Var "X")) ")" ))))) ; 
 
theorem :: BOOLEALG:60 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "X"))  ($#k3_boolealg :::"\+\"::: )  (Set  "(" (Set (Var "X"))  ($#k4_lattices :::""/\""::: )  (Set (Var "Y")) ")" ))  ($#r1_boolealg :::"="::: )  (Set (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set (Var "Y")))))) ; 
 
theorem :: BOOLEALG:61 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "X"))  ($#k3_lattices :::""\/""::: )  (Set (Var "Y")))  ($#r1_boolealg :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k3_boolealg :::"\+\"::: )  (Set (Var "Y")) ")" )  ($#k3_lattices :::""\/""::: )  (Set  "(" (Set (Var "X"))  ($#k4_lattices :::""/\""::: )  (Set (Var "Y")) ")" ))))) ; 
 
theorem :: BOOLEALG:62 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "X"))  ($#k3_boolealg :::"\+\"::: )  (Set (Var "Y")) ")" )  ($#k3_boolealg :::"\+\"::: )  (Set  "(" (Set (Var "X"))  ($#k4_lattices :::""/\""::: )  (Set (Var "Y")) ")" ))  ($#r1_boolealg :::"="::: )  (Set (Set (Var "X"))  ($#k3_lattices :::""\/""::: )  (Set (Var "Y")))))) ; 
 
theorem :: BOOLEALG:63 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "X"))  ($#k3_boolealg :::"\+\"::: )  (Set (Var "Y")) ")" )  ($#k3_boolealg :::"\+\"::: )  (Set  "(" (Set (Var "X"))  ($#k3_lattices :::""\/""::: )  (Set (Var "Y")) ")" ))  ($#r1_boolealg :::"="::: )  (Set (Set (Var "X"))  ($#k4_lattices :::""/\""::: )  (Set (Var "Y")))))) ; 
 
theorem :: BOOLEALG:64 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "X"))  ($#k3_boolealg :::"\+\"::: )  (Set (Var "Y")))  ($#r1_boolealg :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k3_lattices :::""\/""::: )  (Set (Var "Y")) ")" )  ($#k1_boolealg :::"\"::: )  (Set  "(" (Set (Var "X"))  ($#k4_lattices :::""/\""::: )  (Set (Var "Y")) ")" ))))) ; 
 
theorem :: BOOLEALG:65 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "X"))  ($#k3_boolealg :::"\+\"::: )  (Set (Var "Y")) ")" )  ($#k1_boolealg :::"\"::: )  (Set (Var "Z")))  ($#r1_boolealg :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set  "(" (Set (Var "Y"))  ($#k3_lattices :::""\/""::: )  (Set (Var "Z")) ")" ) ")" )  ($#k3_lattices :::""\/""::: )  (Set  "(" (Set (Var "Y"))  ($#k1_boolealg :::"\"::: )  (Set  "(" (Set (Var "X"))  ($#k3_lattices :::""\/""::: )  (Set (Var "Z")) ")" ) ")" ))))) ; 
 
theorem :: BOOLEALG:66 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set  "(" (Set (Var "Y"))  ($#k3_boolealg :::"\+\"::: )  (Set (Var "Z")) ")" ))  ($#r1_boolealg :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k1_boolealg :::"\"::: )  (Set  "(" (Set (Var "Y"))  ($#k3_lattices :::""\/""::: )  (Set (Var "Z")) ")" ) ")" )  ($#k3_lattices :::""\/""::: )  (Set  "(" (Set  "(" (Set (Var "X"))  ($#k4_lattices :::""/\""::: )  (Set (Var "Y")) ")" )  ($#k4_lattices :::""/\""::: )  (Set (Var "Z")) ")" ))))) ; 
 
theorem :: BOOLEALG:67 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "X"))  ($#k3_boolealg :::"\+\"::: )  (Set (Var "Y")) ")" )  ($#k3_boolealg :::"\+\"::: )  (Set (Var "Z")))  ($#r1_boolealg :::"="::: )  (Set (Set (Var "X"))  ($#k3_boolealg :::"\+\"::: )  (Set  "(" (Set (Var "Y"))  ($#k3_boolealg :::"\+\"::: )  (Set (Var "Z")) ")" ))))) ; 
 
theorem :: BOOLEALG:68 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"B_Lattice":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "X"))  ($#k3_boolealg :::"\+\"::: )  (Set (Var "Y")) ")" )  ($#k7_lattices :::"`"::: )  )  ($#r1_boolealg :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k4_lattices :::""/\""::: )  (Set (Var "Y")) ")" )  ($#k3_lattices :::""\/""::: )  (Set  "(" (Set  "(" (Set (Var "X"))  ($#k7_lattices :::"`"::: )  ")" )  ($#k4_lattices :::""/\""::: )  (Set  "(" (Set (Var "Y"))  ($#k7_lattices :::"`"::: )  ")" ) ")" ))))) ;