begin
Lm1:
for X being non empty set
for Y being Subset of (InclPoset X) st ex_sup_of Y, InclPoset X holds
union Y c= sup Y
begin
begin
Lm2:
for L being lower-bounded continuous LATTICE
for B being join-closed Subset of L st Bottom L in B & ( for x, y being Element of L st x << y holds
ex b being Element of L st
( b in B & x <= b & b << y ) ) holds
( the carrier of (CompactSublatt L) c= B & ( for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) ) )
Lm3:
for L being lower-bounded continuous LATTICE
for B being Subset of L st ( for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) ) holds
for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b << y )
Lm4:
for L being lower-bounded continuous LATTICE st L is algebraic holds
( the carrier of (CompactSublatt L) is with_bottom CLbasis of L & ( for B being with_bottom CLbasis of L holds the carrier of (CompactSublatt L) c= B ) )
Lm5:
for L being lower-bounded continuous LATTICE st ex B being with_bottom CLbasis of L st
for B1 being with_bottom CLbasis of L holds B c= B1 holds
L is algebraic