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))

hence
[#] L is CLbasis of L
by WAYBEL23:def 7; :: thesis: verumlet 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;(waybelow x) /\ ([#] L) = waybelow x by XBOOLE_1:28;

hence x = sup ((waybelow x) /\ ([#] L)) by WAYBEL_3:def 5; :: thesis: verum