let L be continuous sup-Semilattice; :: thesis: [#] L is CLbasis of L

now :: thesis: for x being Element of L holds x = sup ((waybelow x) /\ ([#] L))

let x be Element of L; :: thesis: x = sup ((waybelow x) /\ ([#] L))
(waybelow x) /\ ([#] L) = waybelow x by XBOOLE_1:28;
hence x = sup ((waybelow x) /\ ([#] L)) by WAYBEL_3:def 5; :: thesis: verum

end;

hence [#] L is CLbasis of L by WAYBEL23:def 7; :: thesis: verum