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 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;
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