begin
:: deftheorem defines "\/" LATTICES:def 1 :
:: deftheorem defines "/\" LATTICES:def 2 :
:: deftheorem Def3 defines [= LATTICES:def 3 :
Lm1:
for uu, nn being BinOp of (bool {} )
for x, y being Element of LattStr(# (bool {} ),uu,nn #) holds x = y
Lm2:
for n being BinOp of (bool {} )
for x, y being Element of \/-SemiLattStr(# (bool {} ),n #) holds x = y
Lm3:
for n being BinOp of (bool {} )
for x, y being Element of /\-SemiLattStr(# (bool {} ),n #) holds x = y
:: deftheorem Def4 defines join-commutative LATTICES:def 4 :
:: deftheorem Def5 defines join-associative LATTICES:def 5 :
:: deftheorem Def6 defines meet-commutative LATTICES:def 6 :
:: deftheorem Def7 defines meet-associative LATTICES:def 7 :
:: deftheorem Def8 defines meet-absorbing LATTICES:def 8 :
:: deftheorem Def9 defines join-absorbing LATTICES:def 9 :
:: deftheorem Def10 defines Lattice-like LATTICES:def 10 :
:: deftheorem Def11 defines distributive LATTICES:def 11 :
:: deftheorem Def12 defines modular LATTICES:def 12 :
:: deftheorem Def13 defines lower-bounded LATTICES:def 13 :
:: deftheorem Def14 defines upper-bounded LATTICES:def 14 :
Lm4:
for n, u being BinOp of (bool {} ) holds LattStr(# (bool {} ),n,u #) is Lattice
Lm5:
for n, u being BinOp of (bool {} ) holds LattStr(# (bool {} ),n,u #) is 0_Lattice
Lm6:
for n, u being BinOp of (bool {} ) holds LattStr(# (bool {} ),n,u #) is 1_Lattice
:: deftheorem Def15 defines bounded LATTICES:def 15 :
:: deftheorem Def16 defines Bottom LATTICES:def 16 :
:: deftheorem Def17 defines Top LATTICES:def 17 :
:: deftheorem Def18 defines is_a_complement_of LATTICES:def 18 :
:: deftheorem Def19 defines complemented LATTICES:def 19 :
:: deftheorem Def20 defines Boolean LATTICES:def 20 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th17:
theorem
theorem Th19:
theorem
canceled;
theorem Th21:
theorem Th22:
theorem Th23:
theorem
canceled;
theorem
theorem Th26:
theorem Th27:
theorem
canceled;
theorem
theorem
canceled;
theorem Th31:
theorem Th32:
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th39:
theorem
theorem Th41:
theorem
canceled;
theorem Th43:
theorem
theorem
:: deftheorem Def21 defines ` LATTICES:def 21 :
theorem
canceled;
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem
theorem Th52:
theorem
begin
:: deftheorem Defx defines initial LATTICES:def 22 :
:: deftheorem Defy defines final LATTICES:def 23 :
:: deftheorem defines meet-closed LATTICES:def 24 :
:: deftheorem defines join-closed LATTICES:def 25 :
theorem