let L be sup-Semilattice; :: thesis: for x being Element of L holds waybelow x is join-closed
let x be Element of L; :: thesis: waybelow x is join-closed

now

let y, z be Element of L; :: thesis: ( y in the carrier of (subrelstr (waybelow x)) & z in the carrier of (subrelstr (waybelow x)) & ex_sup_of {y,z},L implies sup {y,z} in the carrier of (subrelstr (waybelow x)) )
assume that
A1: y in the carrier of (subrelstr (waybelow x)) and
A2: z in the carrier of (subrelstr (waybelow x)) and
ex_sup_of {y,z},L ; :: thesis: sup {y,z} in the carrier of (subrelstr (waybelow x))
( y in waybelow x & z in waybelow x ) by A1, A2, YELLOW_0:def 15;
then ( y << x & z << x ) by WAYBEL_3:7;
then y "\/" z << x by WAYBEL_3:3;
then y "\/" z in waybelow x by WAYBEL_3:7;
then sup {y,z} in waybelow x by YELLOW_0:41;
hence sup {y,z} in the carrier of (subrelstr (waybelow x)) by YELLOW_0:def 15; :: thesis: verum

end;

then subrelstr (waybelow x) is join-inheriting by YELLOW_0:def 17;
hence waybelow x is join-closed by Def2; :: thesis: verum