:: LATTICE2  semantic presentation begin  
















theorem :: LATTICE2:1 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "C")) "holds"  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set (Var "g"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "B"))))))) ; 
 
theorem :: LATTICE2:2 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "C")) "holds"   (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "B")))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))))  ")" ))))) ; 
 
theorem :: LATTICE2:3 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "C"))  (Bool  "for" (Set (Var "B")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "f"))  ($#k7_funct_4 :::"+*"::: )  (Set  "(" (Set (Var "g"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "B")) ")" )) "is"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "C"))))))) ; 
 
theorem :: LATTICE2:4 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "g")) "," (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "C")) "holds"  (Bool (Set (Set  "(" (Set (Var "g"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "B")) ")" )  ($#k7_funct_4 :::"+*"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "f"))))))) ; 
 
theorem :: LATTICE2:5 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "g"))  ($#r1_tarski :::"c="::: )  (Set (Var "f")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_4 :::"+*"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set (Var "f")))) ; 
 
theorem :: LATTICE2:6 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "C")) "holds"  (Bool (Set (Set (Var "f"))  ($#k7_funct_4 :::"+*"::: )  (Set  "(" (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "f"))))))) ; 
 
theorem :: LATTICE2:7 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "g")) "," (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "C"))  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x"))))  ")" )) "holds"  (Bool (Set (Set (Var "f"))  ($#k7_funct_4 :::"+*"::: )  (Set  "(" (Set (Var "g"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "f"))))))) ; 
 



theorem :: LATTICE2:8 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "g")) "," (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "C"))  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Var "A")) "holds"  (Bool (Set (Set  "(" (Set (Var "g"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "B")) ")" )  ($#k7_funct_4 :::"+*"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "f"))))))) ; 
 
theorem :: LATTICE2:9 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "C"))  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Var "A")) "holds"  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set (Var "g"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "B"))))))) ; 
 
theorem :: LATTICE2:10 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "g")) "," (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "C"))  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Var "A"))  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x"))))  ")" )) "holds"  (Bool (Set (Set (Var "f"))  ($#k7_funct_4 :::"+*"::: )  (Set  "(" (Set (Var "g"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "f"))))))) ; 
 definitionlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "o", "o9" be   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); pred "o" :::"absorbs"::: "o9" means :: LATTICE2:def 1 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" "D" "holds"  (Bool (Set "o"  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set  "(" "o9"  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")"  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "x")))); end; 






:: deftheorem    defines :::"absorbs"::: LATTICE2:def 1 :  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "o")) "," (Set (Var "o9")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "holds"   (Bool  "("  (Bool (Set (Var "o"))  ($#r1_lattice2 :::"absorbs"::: )  (Set (Var "o9"))) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "D")) "holds"  (Bool (Set (Set (Var "o"))  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set  "(" (Set (Var "o9"))  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")"  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "x"))))  ")" ))); 
 notationlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "o", "o9" be   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); antonym "o" :::"doesn't_absorb"::: "o9" for "o" :::"absorbs"::: "o9"; end; 








theorem :: LATTICE2:11 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l3_lattices :::"LattStr"::: )    "st" (Bool (Bool (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" (Set (Var "L"))) "is"   ($#v1_binop_1 :::"commutative"::: )  ) & (Bool (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" (Set (Var "L"))) "is"   ($#v2_binop_1 :::"associative"::: )  ) & (Bool (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set (Var "L"))) "is"   ($#v1_binop_1 :::"commutative"::: )  ) & (Bool (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set (Var "L"))) "is"   ($#v2_binop_1 :::"associative"::: )  ) & (Bool (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" (Set (Var "L")))  ($#r1_lattice2 :::"absorbs"::: )  (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set (Var "L")))) & (Bool (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set (Var "L")))  ($#r1_lattice2 :::"absorbs"::: )  (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" (Set (Var "L"))))) "holds"  (Bool (Set (Var "L")) "is"   ($#v10_lattices :::"Lattice-like"::: )  )) ; 
 definitionlet "L" be    ($#l3_lattices :::"LattStr"::: )  ; func "L" :::".:":::  ->   ($#v3_lattices :::"strict"::: )     ($#l3_lattices :::"LattStr"::: )   equals :: LATTICE2:def 2 (Set   ($#g3_lattices :::"LattStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "L") "," (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" "L") "," (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" "L") "#)" ); end; 





:: deftheorem    defines :::".:"::: LATTICE2:def 2 :  (Bool  "for" (Set (Var "L")) "being"    ($#l3_lattices :::"LattStr"::: )   "holds"  (Bool (Set (Set (Var "L"))  ($#k1_lattice2 :::".:"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#g3_lattices :::"LattStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L"))) "," (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set (Var "L"))) "," (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" (Set (Var "L"))) "#)" ))); 
 registrationlet "L" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l3_lattices :::"LattStr"::: )  ; 
cluster (Set "L"  ($#k1_lattice2 :::".:"::: )  ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_lattices :::"strict"::: )   ; 
end; 
theorem :: LATTICE2:12 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l3_lattices :::"LattStr"::: )   "holds"   (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "(" (Set (Var "L"))  ($#k1_lattice2 :::".:"::: )  ")" ))) & (Bool (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" (Set (Var "L")))  ($#r1_funct_2 :::"="::: )  (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set  "(" (Set (Var "L"))  ($#k1_lattice2 :::".:"::: )  ")" ))) & (Bool (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set (Var "L")))  ($#r1_funct_2 :::"="::: )  (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" (Set  "(" (Set (Var "L"))  ($#k1_lattice2 :::".:"::: )  ")" )))  ")" )) ; 
 
theorem :: LATTICE2:13 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_lattices :::"strict"::: )     ($#l3_lattices :::"LattStr"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "L"))  ($#k1_lattice2 :::".:"::: )  ")" )  ($#k1_lattice2 :::".:"::: )  )  ($#r1_hidden :::"="::: )  (Set (Var "L")))) ; 
 










theorem :: LATTICE2:14 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool  "("   "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "u"))  ($#k3_lattices :::""\/""::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set (Var "v")))  ")" )) "holds"  (Bool (Set (Var "u"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_lattices :::"Bottom"::: )  (Set (Var "L")))))) ; 
 
theorem :: LATTICE2:15 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool  "("   "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" (Set (Var "L")))  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "u")) "," (Set (Var "v")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "v")))  ")" )) "holds"  (Bool (Set (Var "u"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_lattices :::"Bottom"::: )  (Set (Var "L")))))) ; 
 
theorem :: LATTICE2:16 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool  "("   "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "u"))  ($#k4_lattices :::""/\""::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set (Var "v")))  ")" )) "holds"  (Bool (Set (Var "u"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_lattices :::"Top"::: )  (Set (Var "L")))))) ; 
 
theorem :: LATTICE2:17 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool  "("   "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set (Var "L")))  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "u")) "," (Set (Var "v")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "v")))  ")" )) "holds"  (Bool (Set (Var "u"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_lattices :::"Top"::: )  (Set (Var "L")))))) ; 
 registrationlet "L" be   ($#l3_lattices :::"Lattice":::); 
cluster (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" "L") ->   ($#v3_binop_1 :::"idempotent"::: )   ; 
end; registrationlet "L" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v4_lattices :::"join-commutative"::: )     ($#l2_lattices :::"\/-SemiLattStr"::: )  ; 
cluster (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" "L") ->   ($#v1_binop_1 :::"commutative"::: )   ; 
end; 
theorem :: LATTICE2:18 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  "st" (Bool (Bool (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" (Set (Var "L"))) "is"   ($#v1_setwiseo :::"having_a_unity"::: )  )) "holds"  (Bool (Set   ($#k5_lattices :::"Bottom"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_binop_1 :::"the_unity_wrt"::: )  (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" (Set (Var "L")))))) ; 
 registrationlet "L" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v5_lattices :::"join-associative"::: )     ($#l2_lattices :::"\/-SemiLattStr"::: )  ; 
cluster (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" "L") ->   ($#v2_binop_1 :::"associative"::: )   ; 
end; registrationlet "L" be   ($#l3_lattices :::"Lattice":::); 
cluster (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" "L") ->   ($#v3_binop_1 :::"idempotent"::: )   ; 
end; registrationlet "L" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_lattices :::"meet-commutative"::: )     ($#l1_lattices :::"/\-SemiLattStr"::: )  ; 
cluster (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" "L") ->   ($#v1_binop_1 :::"commutative"::: )   ; 
end; registrationlet "L" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v7_lattices :::"meet-associative"::: )     ($#l1_lattices :::"/\-SemiLattStr"::: )  ; 
cluster (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" "L") ->   ($#v2_binop_1 :::"associative"::: )   ; 
end; 
theorem :: LATTICE2:19 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  "st" (Bool (Bool (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set (Var "L"))) "is"   ($#v1_setwiseo :::"having_a_unity"::: )  )) "holds"  (Bool (Set   ($#k6_lattices :::"Top"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_binop_1 :::"the_unity_wrt"::: )  (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set (Var "L")))))) ; 
 
theorem :: LATTICE2:20 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::) "holds"  (Bool (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" (Set (Var "L")))  ($#r6_binop_1 :::"is_distributive_wrt"::: )  (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" (Set (Var "L"))))) ; 
 
theorem :: LATTICE2:21 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  "st" (Bool (Bool (Set (Var "L")) "is"   ($#l3_lattices :::"D_Lattice":::))) "holds"  (Bool (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" (Set (Var "L")))  ($#r6_binop_1 :::"is_distributive_wrt"::: )  (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set (Var "L"))))) ; 
 
theorem :: LATTICE2:22 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  "st" (Bool (Bool (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" (Set (Var "L")))  ($#r6_binop_1 :::"is_distributive_wrt"::: )  (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set (Var "L"))))) "holds"  (Bool (Set (Var "L")) "is"   ($#v11_lattices :::"distributive"::: )  )) ; 
 
theorem :: LATTICE2:23 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  "st" (Bool (Bool (Set (Var "L")) "is"   ($#l3_lattices :::"D_Lattice":::))) "holds"  (Bool (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set (Var "L")))  ($#r6_binop_1 :::"is_distributive_wrt"::: )  (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" (Set (Var "L"))))) ; 
 
theorem :: LATTICE2:24 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  "st" (Bool (Bool (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set (Var "L")))  ($#r6_binop_1 :::"is_distributive_wrt"::: )  (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" (Set (Var "L"))))) "holds"  (Bool (Set (Var "L")) "is"   ($#v11_lattices :::"distributive"::: )  )) ; 
 
theorem :: LATTICE2:25 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::) "holds"  (Bool (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set (Var "L")))  ($#r6_binop_1 :::"is_distributive_wrt"::: )  (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set (Var "L"))))) ; 
 
theorem :: LATTICE2:26 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::) "holds"  (Bool (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" (Set (Var "L")))  ($#r1_lattice2 :::"absorbs"::: )  (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set (Var "L"))))) ; 
 
theorem :: LATTICE2:27 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::) "holds"  (Bool (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set (Var "L")))  ($#r1_lattice2 :::"absorbs"::: )  (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" (Set (Var "L"))))) ; 
 definitionlet "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "L" be   ($#l3_lattices :::"Lattice":::); let "B" be   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Const "A")); let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "A")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Const "L"))); func  :::"FinJoin":::  "(" "B" "," "f" ")"  ->   ($#m1_subset_1 :::"Element":::) "of" "L" equals :: LATTICE2:def 3 (Set (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" "L")  ($#k7_setwiseo :::"$$"::: )   "(" "B" "," "f" ")" ); func  :::"FinMeet":::  "(" "B" "," "f" ")"  ->   ($#m1_subset_1 :::"Element":::) "of" "L" equals :: LATTICE2:def 4 (Set (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" "L")  ($#k7_setwiseo :::"$$"::: )   "(" "B" "," "f" ")" ); end; 
















:: deftheorem    defines :::"FinJoin"::: LATTICE2:def 3 :  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L"))) "holds"  (Bool (Set   ($#k2_lattice2 :::"FinJoin"::: )   "(" (Set (Var "B")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" (Set (Var "L")))  ($#k7_setwiseo :::"$$"::: )   "(" (Set (Var "B")) "," (Set (Var "f")) ")" )))))); 
 
:: deftheorem    defines :::"FinMeet"::: LATTICE2:def 4 :  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L"))) "holds"  (Bool (Set   ($#k3_lattice2 :::"FinMeet"::: )   "(" (Set (Var "B")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set (Var "L")))  ($#k7_setwiseo :::"$$"::: )   "(" (Set (Var "B")) "," (Set (Var "f")) ")" )))))); 
 













theorem :: LATTICE2:28 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r3_lattices :::"[="::: )  (Set   ($#k2_lattice2 :::"FinJoin"::: )   "(" (Set (Var "B")) "," (Set (Var "f")) ")" ))))))) ; 
 
theorem :: LATTICE2:29 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))  "st" (Bool (Bool  "ex" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A")) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) & (Bool (Set (Var "u"))  ($#r3_lattices :::"[="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x"))))  ")" ))) "holds"  (Bool (Set (Var "u"))  ($#r3_lattices :::"[="::: )  (Set   ($#k2_lattice2 :::"FinJoin"::: )   "(" (Set (Var "B")) "," (Set (Var "f")) ")" ))))))) ; 
 
theorem :: LATTICE2:30 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "u")))  ")" ) & (Bool (Set (Var "B"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set   ($#k2_lattice2 :::"FinJoin"::: )   "(" (Set (Var "B")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "u")))))))) ; 
 
theorem :: LATTICE2:31 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))  "st" (Bool (Bool (Set   ($#k2_lattice2 :::"FinJoin"::: )   "(" (Set (Var "B")) "," (Set (Var "f")) ")" )  ($#r3_lattices :::"[="::: )  (Set (Var "u")))) "holds"  (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r3_lattices :::"[="::: )  (Set (Var "u"))))))))) ; 
 
theorem :: LATTICE2:32 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r3_lattices :::"[="::: )  (Set (Var "u")))  ")" )) "holds"  (Bool (Set   ($#k2_lattice2 :::"FinJoin"::: )   "(" (Set (Var "B")) "," (Set (Var "f")) ")" )  ($#r3_lattices :::"[="::: )  (Set (Var "u")))))))) ; 
 
theorem :: LATTICE2:33 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r3_lattices :::"[="::: )  (Set (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x"))))  ")" )) "holds"  (Bool (Set   ($#k2_lattice2 :::"FinJoin"::: )   "(" (Set (Var "B")) "," (Set (Var "f")) ")" )  ($#r3_lattices :::"[="::: )  (Set   ($#k2_lattice2 :::"FinJoin"::: )   "(" (Set (Var "B")) "," (Set (Var "g")) ")" )))))) ; 
 
theorem :: LATTICE2:34 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "B"))))) "holds"  (Bool (Set   ($#k2_lattice2 :::"FinJoin"::: )   "(" (Set (Var "B")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k2_lattice2 :::"FinJoin"::: )   "(" (Set (Var "B")) "," (Set (Var "g")) ")" )))))) ; 
 
theorem :: LATTICE2:35 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set (Set (Var "v"))  ($#k3_lattices :::""\/""::: )  (Set  "("  ($#k2_lattice2 :::"FinJoin"::: )   "(" (Set (Var "B")) "," (Set (Var "f")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_lattice2 :::"FinJoin"::: )   "(" (Set (Var "B")) "," (Set  "(" (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" (Set (Var "L")))  ($#k10_funcop_1 :::"[;]"::: )   "(" (Set (Var "v")) "," (Set (Var "f")) ")"  ")" ) ")" ))))))) ; 
 registrationlet "L" be   ($#l3_lattices :::"Lattice":::); 
cluster (Set "L"  ($#k1_lattice2 :::".:"::: )  ) ->   ($#v3_lattices :::"strict"::: )     ($#v10_lattices :::"Lattice-like"::: )   ; 
end; 
theorem :: LATTICE2:36 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))  (Bool  "for" (Set (Var "f9")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "(" (Set (Var "L"))  ($#k1_lattice2 :::".:"::: )  ")" ))  "st" (Bool (Bool (Set (Var "f"))  ($#r1_funct_2 :::"="::: )  (Set (Var "f9")))) "holds"  (Bool  "("  (Bool (Set   ($#k2_lattice2 :::"FinJoin"::: )   "(" (Set (Var "B")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_lattice2 :::"FinMeet"::: )   "(" (Set (Var "B")) "," (Set (Var "f9")) ")" )) & (Bool (Set   ($#k3_lattice2 :::"FinMeet"::: )   "(" (Set (Var "B")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k2_lattice2 :::"FinJoin"::: )   "(" (Set (Var "B")) "," (Set (Var "f9")) ")" ))  ")" )))))) ; 
 
theorem :: LATTICE2:37 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  (Bool  "for" (Set (Var "a9")) "," (Set (Var "b9")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Var "L"))  ($#k1_lattice2 :::".:"::: )  ")" )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "a9"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "b9")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "a"))  ($#k4_lattices :::""/\""::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a9"))  ($#k3_lattices :::""\/""::: )  (Set (Var "b9")))) & (Bool (Set (Set (Var "a"))  ($#k3_lattices :::""\/""::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a9"))  ($#k4_lattices :::""/\""::: )  (Set (Var "b9"))))  ")" )))) ; 
 
theorem :: LATTICE2:38 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "a"))  ($#r3_lattices :::"[="::: )  (Set (Var "b")))) "holds"  (Bool  "for" (Set (Var "a9")) "," (Set (Var "b9")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Var "L"))  ($#k1_lattice2 :::".:"::: )  ")" )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "a9"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "b9")))) "holds"  (Bool (Set (Var "b9"))  ($#r3_lattices :::"[="::: )  (Set (Var "a9")))))) ; 
 
theorem :: LATTICE2:39 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  (Bool  "for" (Set (Var "a9")) "," (Set (Var "b9")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Var "L"))  ($#k1_lattice2 :::".:"::: )  ")" )  "st" (Bool (Bool (Set (Var "a9"))  ($#r3_lattices :::"[="::: )  (Set (Var "b9"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "a9"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "b9")))) "holds"  (Bool (Set (Var "b"))  ($#r3_lattices :::"[="::: )  (Set (Var "a")))))) ; 
 
theorem :: LATTICE2:40 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))) "holds"  (Bool (Set   ($#k3_lattice2 :::"FinMeet"::: )   "(" (Set (Var "B")) "," (Set (Var "f")) ")" )  ($#r3_lattices :::"[="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x"))))))))) ; 
 
theorem :: LATTICE2:41 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))  "st" (Bool (Bool  "ex" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A")) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) & (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r3_lattices :::"[="::: )  (Set (Var "u")))  ")" ))) "holds"  (Bool (Set   ($#k3_lattice2 :::"FinMeet"::: )   "(" (Set (Var "B")) "," (Set (Var "f")) ")" )  ($#r3_lattices :::"[="::: )  (Set (Var "u")))))))) ; 
 
theorem :: LATTICE2:42 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "u")))  ")" ) & (Bool (Set (Var "B"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set   ($#k3_lattice2 :::"FinMeet"::: )   "(" (Set (Var "B")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "u")))))))) ; 
 
theorem :: LATTICE2:43 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set (Set (Var "v"))  ($#k4_lattices :::""/\""::: )  (Set  "("  ($#k3_lattice2 :::"FinMeet"::: )   "(" (Set (Var "B")) "," (Set (Var "f")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_lattice2 :::"FinMeet"::: )   "(" (Set (Var "B")) "," (Set  "(" (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set (Var "L")))  ($#k10_funcop_1 :::"[;]"::: )   "(" (Set (Var "v")) "," (Set (Var "f")) ")"  ")" ) ")" ))))))) ; 
 
theorem :: LATTICE2:44 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))  "st" (Bool (Bool (Set (Var "u"))  ($#r3_lattices :::"[="::: )  (Set   ($#k3_lattice2 :::"FinMeet"::: )   "(" (Set (Var "B")) "," (Set (Var "f")) ")" ))) "holds"  (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Var "u"))  ($#r3_lattices :::"[="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))))))))) ; 
 
theorem :: LATTICE2:45 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "B"))))) "holds"  (Bool (Set   ($#k3_lattice2 :::"FinMeet"::: )   "(" (Set (Var "B")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_lattice2 :::"FinMeet"::: )   "(" (Set (Var "B")) "," (Set (Var "g")) ")" )))))) ; 
 
theorem :: LATTICE2:46 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Var "u"))  ($#r3_lattices :::"[="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x"))))  ")" )) "holds"  (Bool (Set (Var "u"))  ($#r3_lattices :::"[="::: )  (Set   ($#k3_lattice2 :::"FinMeet"::: )   "(" (Set (Var "B")) "," (Set (Var "f")) ")" ))))))) ; 
 
theorem :: LATTICE2:47 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::)  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r3_lattices :::"[="::: )  (Set (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x"))))  ")" )) "holds"  (Bool (Set   ($#k3_lattice2 :::"FinMeet"::: )   "(" (Set (Var "B")) "," (Set (Var "f")) ")" )  ($#r3_lattices :::"[="::: )  (Set   ($#k3_lattice2 :::"FinMeet"::: )   "(" (Set (Var "B")) "," (Set (Var "g")) ")" )))))) ; 
 
theorem :: LATTICE2:48 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::) "holds"   (Bool  "("  (Bool (Set (Var "L")) "is"   ($#v13_lattices :::"lower-bounded"::: )  ) "iff" (Bool (Set (Set (Var "L"))  ($#k1_lattice2 :::".:"::: )  ) "is"   ($#v14_lattices :::"upper-bounded"::: )  )  ")" )) ; 
 
theorem :: LATTICE2:49 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::) "holds"   (Bool  "("  (Bool (Set (Var "L")) "is"   ($#v14_lattices :::"upper-bounded"::: )  ) "iff" (Bool (Set (Set (Var "L"))  ($#k1_lattice2 :::".:"::: )  ) "is"   ($#v13_lattices :::"lower-bounded"::: )  )  ")" )) ; 
 
theorem :: LATTICE2:50 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::) "holds"   (Bool  "("  (Bool (Set (Var "L")) "is"   ($#l3_lattices :::"D_Lattice":::)) "iff" (Bool (Set (Set (Var "L"))  ($#k1_lattice2 :::".:"::: )  ) "is"   ($#l3_lattices :::"D_Lattice":::))  ")" )) ; 
 










theorem :: LATTICE2:51 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"0_Lattice":::) "holds"  (Bool (Set   ($#k5_lattices :::"Bottom"::: )  (Set (Var "L")))  ($#r3_binop_1 :::"is_a_unity_wrt"::: )  (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" (Set (Var "L"))))) ; 
 registrationlet "L" be   ($#l3_lattices :::"0_Lattice":::); 
cluster (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" "L") ->   ($#v1_setwiseo :::"having_a_unity"::: )   ; 
end; 
theorem :: LATTICE2:52 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"0_Lattice":::) "holds"  (Bool (Set   ($#k5_lattices :::"Bottom"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_binop_1 :::"the_unity_wrt"::: )  (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" (Set (Var "L")))))) ; 
 
theorem :: LATTICE2:53 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"0_Lattice":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "B"))))) "holds"  (Bool (Set   ($#k2_lattice2 :::"FinJoin"::: )   "(" (Set (Var "B")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k2_lattice2 :::"FinJoin"::: )   "(" (Set (Var "B")) "," (Set (Var "g")) ")" )))))) ; 
 
theorem :: LATTICE2:54 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"0_Lattice":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))  (Bool  "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r3_lattices :::"[="::: )  (Set (Var "u")))  ")" )) "holds"  (Bool (Set   ($#k2_lattice2 :::"FinJoin"::: )   "(" (Set (Var "B")) "," (Set (Var "f")) ")" )  ($#r3_lattices :::"[="::: )  (Set (Var "u")))))))) ; 
 
theorem :: LATTICE2:55 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"0_Lattice":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r3_lattices :::"[="::: )  (Set (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x"))))  ")" )) "holds"  (Bool (Set   ($#k2_lattice2 :::"FinJoin"::: )   "(" (Set (Var "B")) "," (Set (Var "f")) ")" )  ($#r3_lattices :::"[="::: )  (Set   ($#k2_lattice2 :::"FinJoin"::: )   "(" (Set (Var "B")) "," (Set (Var "g")) ")" )))))) ; 
 










theorem :: LATTICE2:56 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"1_Lattice":::) "holds"  (Bool (Set   ($#k6_lattices :::"Top"::: )  (Set (Var "L")))  ($#r3_binop_1 :::"is_a_unity_wrt"::: )  (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set (Var "L"))))) ; 
 registrationlet "L" be   ($#l3_lattices :::"1_Lattice":::); 
cluster (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" "L") ->   ($#v1_setwiseo :::"having_a_unity"::: )   ; 
end; 
theorem :: LATTICE2:57 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"1_Lattice":::) "holds"  (Bool (Set   ($#k6_lattices :::"Top"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_binop_1 :::"the_unity_wrt"::: )  (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set (Var "L")))))) ; 
 
theorem :: LATTICE2:58 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"1_Lattice":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "B"))))) "holds"  (Bool (Set   ($#k3_lattice2 :::"FinMeet"::: )   "(" (Set (Var "B")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_lattice2 :::"FinMeet"::: )   "(" (Set (Var "B")) "," (Set (Var "g")) ")" )))))) ; 
 
theorem :: LATTICE2:59 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"1_Lattice":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))  (Bool  "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Var "u"))  ($#r3_lattices :::"[="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x"))))  ")" )) "holds"  (Bool (Set (Var "u"))  ($#r3_lattices :::"[="::: )  (Set   ($#k3_lattice2 :::"FinMeet"::: )   "(" (Set (Var "B")) "," (Set (Var "f")) ")" ))))))) ; 
 
theorem :: LATTICE2:60 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"1_Lattice":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r3_lattices :::"[="::: )  (Set (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x"))))  ")" )) "holds"  (Bool (Set   ($#k3_lattice2 :::"FinMeet"::: )   "(" (Set (Var "B")) "," (Set (Var "f")) ")" )  ($#r3_lattices :::"[="::: )  (Set   ($#k3_lattice2 :::"FinMeet"::: )   "(" (Set (Var "B")) "," (Set (Var "g")) ")" )))))) ; 
 
theorem :: LATTICE2:61 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"0_Lattice":::) "holds"  (Bool (Set   ($#k5_lattices :::"Bottom"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_lattices :::"Top"::: )  (Set  "(" (Set (Var "L"))  ($#k1_lattice2 :::".:"::: )  ")" )))) ; 
 
theorem :: LATTICE2:62 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"1_Lattice":::) "holds"  (Bool (Set   ($#k6_lattices :::"Top"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_lattices :::"Bottom"::: )  (Set  "(" (Set (Var "L"))  ($#k1_lattice2 :::".:"::: )  ")" )))) ; 
 definitionmode D0_Lattice is   ($#v11_lattices :::"distributive"::: )     ($#v13_lattices :::"lower-bounded"::: )    ($#l3_lattices :::"Lattice":::); end; 










theorem :: LATTICE2:63 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"D0_Lattice":::) "holds"  (Bool (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set (Var "L")))  ($#r6_binop_1 :::"is_distributive_wrt"::: )  (Set  "the"  ($#u2_lattices :::"L_join"::: )  "of" (Set (Var "L"))))) ; 
 
theorem :: LATTICE2:64 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"D0_Lattice":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))  (Bool  "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set (Var "L")))  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "u")) "," (Set  "("  ($#k2_lattice2 :::"FinJoin"::: )   "(" (Set (Var "B")) "," (Set (Var "f")) ")"  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k2_lattice2 :::"FinJoin"::: )   "(" (Set (Var "B")) "," (Set  "(" (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set (Var "L")))  ($#k10_funcop_1 :::"[;]"::: )   "(" (Set (Var "u")) "," (Set (Var "f")) ")"  ")" ) ")" ))))))) ; 
 
theorem :: LATTICE2:65 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"D0_Lattice":::)  (Bool  "for" (Set (Var "g")) "," (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))  (Bool  "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "g"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "u"))  ($#k4_lattices :::""/\""::: )  (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" )))  ")" )) "holds"  (Bool (Set (Set (Var "u"))  ($#k4_lattices :::""/\""::: )  (Set  "("  ($#k2_lattice2 :::"FinJoin"::: )   "(" (Set (Var "B")) "," (Set (Var "f")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_lattice2 :::"FinJoin"::: )   "(" (Set (Var "B")) "," (Set (Var "g")) ")" ))))))) ; 
 
theorem :: LATTICE2:66 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Finite_Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"D0_Lattice":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "L")))  (Bool  "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "u"))  ($#k4_lattices :::""/\""::: )  (Set  "("  ($#k2_lattice2 :::"FinJoin"::: )   "(" (Set (Var "B")) "," (Set (Var "f")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_lattice2 :::"FinJoin"::: )   "(" (Set (Var "B")) "," (Set  "(" (Set  "the"  ($#u1_lattices :::"L_meet"::: )  "of" (Set (Var "L")))  ($#k10_funcop_1 :::"[;]"::: )   "(" (Set (Var "u")) "," (Set (Var "f")) ")"  ")" ) ")" ))))))) ; 
 definitionlet "IT" be   ($#l3_lattices :::"Lattice":::); attr "IT" is  :::"Heyting":::  means :: LATTICE2:def 5 (Bool  "("  (Bool "IT" "is"   ($#v3_filter_0 :::"implicative"::: )  ) & (Bool "IT" "is"   ($#v13_lattices :::"lower-bounded"::: )  )  ")" ); end; 




:: deftheorem    defines :::"Heyting"::: LATTICE2:def 5 :  (Bool  "for" (Set (Var "IT")) "being"   ($#l3_lattices :::"Lattice":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_lattice2 :::"Heyting"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v3_filter_0 :::"implicative"::: )  ) & (Bool (Set (Var "IT")) "is"   ($#v13_lattices :::"lower-bounded"::: )  )  ")" )  ")" )); 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#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"::: )     ($#v1_lattice2 :::"Heyting"::: )    for    ($#l3_lattices :::"LattStr"::: )  ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_lattices :::"Lattice-like"::: )     ($#v1_lattice2 :::"Heyting"::: )    ->   ($#v13_lattices :::"lower-bounded"::: )     ($#v3_filter_0 :::"implicative"::: )    for    ($#l3_lattices :::"LattStr"::: )  ; 

cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v10_lattices :::"Lattice-like"::: )     ($#v13_lattices :::"lower-bounded"::: )     ($#v3_filter_0 :::"implicative"::: )    ->   ($#v1_lattice2 :::"Heyting"::: )    for    ($#l3_lattices :::"LattStr"::: )  ; 
end; definitionmode H_Lattice is   ($#v1_lattice2 :::"Heyting"::: )    ($#l3_lattices :::"Lattice":::); end; 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"::: )     ($#v1_lattice2 :::"Heyting"::: )    for    ($#l3_lattices :::"LattStr"::: )  ; 
end; 
theorem :: LATTICE2:67 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"0_Lattice":::) "holds"   (Bool  "("  (Bool (Set (Var "L")) "is"   ($#l3_lattices :::"H_Lattice":::)) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool  "ex" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st"  (Bool  "("  (Bool (Set (Set (Var "x"))  ($#k4_lattices :::""/\""::: )  (Set (Var "y")))  ($#r3_lattices :::"[="::: )  (Set (Var "z"))) & (Bool  "("   "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Set (Var "x"))  ($#k4_lattices :::""/\""::: )  (Set (Var "v")))  ($#r3_lattices :::"[="::: )  (Set (Var "z")))) "holds"  (Bool (Set (Var "v"))  ($#r3_lattices :::"[="::: )  (Set (Var "y")))  ")" )  ")" )))  ")" )) ; 
 
theorem :: LATTICE2:68 (Bool  "for" (Set (Var "L")) "being"   ($#l3_lattices :::"Lattice":::) "holds"   (Bool  "("  (Bool (Set (Var "L")) "is"   ($#v8_struct_0 :::"finite"::: )  ) "iff" (Bool (Set (Set (Var "L"))  ($#k1_lattice2 :::".:"::: )  ) "is"   ($#v8_struct_0 :::"finite"::: )  )  ")" )) ; 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v8_struct_0 :::"finite"::: )     ($#v10_lattices :::"Lattice-like"::: )    ->   ($#v13_lattices :::"lower-bounded"::: )    for    ($#l3_lattices :::"LattStr"::: )  ; 

cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v8_struct_0 :::"finite"::: )     ($#v10_lattices :::"Lattice-like"::: )    ->   ($#v14_lattices :::"upper-bounded"::: )    for    ($#l3_lattices :::"LattStr"::: )  ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v8_struct_0 :::"finite"::: )     ($#v10_lattices :::"Lattice-like"::: )    ->   ($#v15_lattices :::"bounded"::: )    for    ($#l3_lattices :::"LattStr"::: )  ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v8_struct_0 :::"finite"::: )     ($#v10_lattices :::"Lattice-like"::: )     ($#v11_lattices :::"distributive"::: )    ->   ($#v1_lattice2 :::"Heyting"::: )    for    ($#l3_lattices :::"LattStr"::: )  ; 
end;