for L being lower-bounded continuous LATTICE holds
( L is algebraic iff ( 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, Lm5;