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

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