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

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

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)

then A2:
L is satisfying_axiom_K
by WAYBEL_8:def 3;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;x = sup ((waybelow x) /\ C) by A1, Def7;

hence x = sup (compactbelow x) by Th1; :: thesis: verum

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