take S = [#] L; :: thesis: ( S is join-closed & ( for x being Element of L holds x = sup ((waybelow x) /\ S) ) )
subrelstr S is join-inheriting by WAYBEL_0:64;
hence S is join-closed ; :: thesis: for x being Element of L holds x = sup ((waybelow x) /\ S)
let x be Element of L; :: thesis: x = sup ((waybelow x) /\ S)
thus x = sup (waybelow x) by WAYBEL_3:def 5
.= sup ((waybelow x) /\ S) by XBOOLE_1:28 ; :: thesis: verum