let L be lower-bounded continuous sup-Semilattice; :: thesis: ( the carrier of (CompactSublatt L) is CLbasis of L implies L is algebraic )
reconsider C = the carrier of (CompactSublatt L) as Subset of L by Th43;
assume A1: the carrier of (CompactSublatt L) is CLbasis of L ; :: thesis: L is algebraic
now :: thesis: for x being Element of L holds x = sup (compactbelow x)
let x be Element of L; :: thesis: x = sup (compactbelow x)
x = sup ((waybelow x) /\ C) by A1, Def7;
hence x = sup (compactbelow x) by Th1; :: thesis: verum
end;
then A2: L is satisfying_axiom_K by WAYBEL_8:def 3;
for x being Element of L holds
( not compactbelow x is empty & compactbelow x is directed ) ;
hence L is algebraic by A2, WAYBEL_8:def 4; :: thesis: verum