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 )

proof

assume 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 ( 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 ) ) by Lm4;
hence ex B being with_bottom CLbasis of L st
for B1 being with_bottom CLbasis of L holds B c= B1 ; :: thesis: verum

end;

thus ( 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 ) by Lm5; :: thesis: verum