let L be lower-bounded continuous LATTICE; :: thesis: ( L is algebraic implies ( 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 ) ) )
assume L is algebraic ; :: thesis: ( 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 ) )
hence the carrier of (CompactSublatt L) is with_bottom CLbasis of L by Th44; :: thesis: for B being with_bottom CLbasis of L holds the carrier of (CompactSublatt L) c= B
let B be with_bottom CLbasis of L; :: thesis: the carrier of (CompactSublatt L) c= B
Bottom L in B by Def8;
hence the carrier of (CompactSublatt L) c= B by Th48; :: thesis: verum