begin
theorem
theorem Th2:
theorem
theorem
theorem
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
begin
theorem Th11:
:: deftheorem defines \ YELLOW_5:def 1 :
:: deftheorem defines \+\ YELLOW_5:def 2 :
Lm1:
for L being antisymmetric with_suprema with_infima RelStr
for a, b being Element of holds a \+\ b = b \+\ a
:: deftheorem Def3 defines meets YELLOW_5:def 3 :
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
canceled;
theorem
theorem Th20:
theorem
begin
theorem Th22:
theorem
theorem
theorem
theorem
theorem
theorem Th28:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
begin
theorem
theorem Th37:
theorem
theorem Th39:
theorem Th40:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th65:
theorem
theorem
theorem
theorem
theorem
theorem
theorem