A2: 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;

for x, y being Element of L st x in [#] L & y in [#] L holds
sup {x,y} in [#] L ;
then [#] L is join-closed by Th18;
then reconsider S = [#] L as CLbasis of L by A2, Def7;
take S ; :: thesis: S is with_top
thus S is with_top ; :: thesis: verum