let L be lower-bounded continuous LATTICE; :: thesis: ( L is algebraic iff ex B being with_bottom CLbasis of L st

for B1 being with_bottom CLbasis of L holds B c= B1 )

thus ( L is algebraic implies ex B being with_bottom CLbasis of L st

for B1 being with_bottom CLbasis of L holds B c= B1 ) :: thesis: ( ex B being with_bottom CLbasis of L st

for B1 being with_bottom CLbasis of L holds B c= B1 implies L is algebraic )

for B1 being with_bottom CLbasis of L holds B c= B1 implies L is algebraic ) by Lm5; :: thesis: verum

for B1 being with_bottom CLbasis of L holds B c= B1 )

thus ( L is algebraic implies ex B being with_bottom CLbasis of L st

for B1 being with_bottom CLbasis of L holds B c= B1 ) :: thesis: ( ex B being with_bottom CLbasis of L st

for B1 being with_bottom CLbasis of L holds B c= B1 implies L is algebraic )

proof

thus
( ex B being with_bottom CLbasis of L st
assume A1:
L is algebraic
; :: thesis: ex B being with_bottom CLbasis of L st

for B1 being with_bottom CLbasis of L holds B c= B1

then A2: for B being with_bottom CLbasis of L holds the carrier of (CompactSublatt L) c= B by Lm4;

the carrier of (CompactSublatt L) is with_bottom CLbasis of L by A1, Lm4;

hence ex B being with_bottom CLbasis of L st

for B1 being with_bottom CLbasis of L holds B c= B1 by A2; :: thesis: verum

end;for B1 being with_bottom CLbasis of L holds B c= B1

then A2: for B being with_bottom CLbasis of L holds the carrier of (CompactSublatt L) c= B by Lm4;

the carrier of (CompactSublatt L) is with_bottom CLbasis of L by A1, Lm4;

hence ex B being with_bottom CLbasis of L st

for B1 being with_bottom CLbasis of L holds B c= B1 by A2; :: thesis: verum

for B1 being with_bottom CLbasis of L holds B c= B1 implies L is algebraic ) by Lm5; :: thesis: verum