for x, y being Element of L st x in [#] L & y in [#] L holds
sup {x,y} in [#] L ;
then A1: [#] L is join-closed by Th18;

now

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;

then reconsider S = [#] L as CLbasis of L by A1, Def7;
take S ; :: thesis: S is with_bottom
Bottom L in [#] L ;
hence S is with_bottom by Def8; :: thesis: verum