begin
:: deftheorem defines c= LATTICE7:def 1 :
:: deftheorem Def2 defines Chain LATTICE7:def 2 :
theorem Th1:
:: deftheorem Def3 defines height LATTICE7:def 3 :
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem
theorem Th7:
begin
:: deftheorem Def4 defines <(1) LATTICE7:def 4 :
for
L being
LATTICE for
x,
y being
Element of holds
(
x <(1) y iff (
x < y & ( for
z being
Element of holds
( not
x < z or not
z < y ) ) ) );
theorem Th8:
:: deftheorem Def5 defines max LATTICE7:def 5 :
theorem Th9:
:: deftheorem defines Join-IRR LATTICE7:def 6 :
theorem Th10:
theorem Th11:
Lm1:
for L being finite distributive LATTICE
for a being Element of st ( for b being Element of st b < a holds
sup ((downarrow b) /\ (Join-IRR L)) = b ) holds
sup ((downarrow a) /\ (Join-IRR L)) = a
theorem Th12:
begin
:: deftheorem defines LOWER LATTICE7:def 7 :
theorem Th13:
theorem Th14:
:: deftheorem Def8 defines Ring_of_sets LATTICE7:def 8 :
Lm2:
for L1, L2 being non empty RelStr
for f being Function of L1,L2 st f is infs-preserving holds
f is meet-preserving
Lm3:
for L1, L2 being non empty RelStr
for f being Function of L1,L2 st f is sups-preserving holds
f is join-preserving
theorem Th15:
theorem