begin
Lm1:
for S, T being non empty with_suprema Poset
for f being Function of S,T st f is directed-sups-preserving holds
f is monotone
begin
begin
begin
begin
Lm2:
for L being complete continuous LATTICE st ( for l being Element of L ex X being Subset of L st
( l = sup X & ( for x being Element of L st x in X holds
x is co-prime ) ) ) holds
L is completely-distributive
Lm3:
for L being complete completely-distributive LATTICE holds
( L is distributive & L is continuous & L ~ is continuous )
Lm4:
for L being complete LATTICE st L is distributive & L is continuous & L ~ is continuous holds
for l being Element of L ex X being Subset of L st
( l = sup X & ( for x being Element of L st x in X holds
x is co-prime ) )