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

for x, y being Element of L st x in [#] L & y in [#] L holds 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;(waybelow x) /\ ([#] L) = waybelow x by XBOOLE_1:28;

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

sup {x,y} in [#] L ;

then [#] L is join-closed by Th18;

then reconsider S = [#] L as CLbasis of L by A1, Def7;

take S ; :: thesis: S is with_bottom

thus S is with_bottom ; :: thesis: verum