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

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