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