begin
:: deftheorem defines \ BOOLEALG:def 1 :
:: deftheorem defines \+\ BOOLEALG:def 2 :
:: deftheorem Def3 defines = BOOLEALG:def 3 :
:: deftheorem Def4 defines meets BOOLEALG:def 4 :
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
Lm1:
for L being Lattice
for X, Y being Element of L st X meets Y holds
Y meets X
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
begin
begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
begin
theorem
canceled;
theorem
canceled;
theorem Th25:
theorem
theorem Th27:
theorem
theorem
canceled;
theorem Th30:
theorem Th31:
theorem
theorem
theorem
theorem
theorem
theorem
begin
theorem
theorem Th39:
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th46:
theorem
theorem
theorem
theorem Th50:
theorem
theorem Th52:
theorem Th53:
theorem Th54:
theorem
theorem
theorem
theorem
theorem Th59:
theorem
theorem Th61:
theorem Th62:
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th67:
theorem
theorem Th69:
theorem Th70:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
Lm2:
for L being B_Lattice
for X, Y being Element of L holds (X "\/" Y) \ (X \+\ Y) = X "/\" Y
theorem
theorem
theorem Th84:
theorem
theorem
theorem
theorem