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

let x be Element of L; :: thesis: wayabove x is join-closed

hence wayabove x is join-closed ; :: thesis: verum

let x be Element of L; :: thesis: wayabove x is join-closed

now :: thesis: for y, z being Element of L st y in the carrier of (subrelstr (wayabove x)) & z in the carrier of (subrelstr (wayabove x)) & ex_sup_of {y,z},L holds

sup {y,z} in the carrier of (subrelstr (wayabove x))

then
subrelstr (wayabove x) is join-inheriting
;sup {y,z} in the carrier of (subrelstr (wayabove x))

let y, z be Element of L; :: thesis: ( y in the carrier of (subrelstr (wayabove x)) & z in the carrier of (subrelstr (wayabove x)) & ex_sup_of {y,z},L implies sup {y,z} in the carrier of (subrelstr (wayabove x)) )

assume that

A1: y in the carrier of (subrelstr (wayabove x)) and

z in the carrier of (subrelstr (wayabove x)) and

ex_sup_of {y,z},L ; :: thesis: sup {y,z} in the carrier of (subrelstr (wayabove x))

y in wayabove x by A1, YELLOW_0:def 15;

then A2: y >> x by WAYBEL_3:8;

y "\/" z >= y by YELLOW_0:22;

then y "\/" z >> x by A2, WAYBEL_3:2;

then y "\/" z in wayabove x by WAYBEL_3:8;

then sup {y,z} in wayabove x by YELLOW_0:41;

hence sup {y,z} in the carrier of (subrelstr (wayabove x)) by YELLOW_0:def 15; :: thesis: verum

end;assume that

A1: y in the carrier of (subrelstr (wayabove x)) and

z in the carrier of (subrelstr (wayabove x)) and

ex_sup_of {y,z},L ; :: thesis: sup {y,z} in the carrier of (subrelstr (wayabove x))

y in wayabove x by A1, YELLOW_0:def 15;

then A2: y >> x by WAYBEL_3:8;

y "\/" z >= y by YELLOW_0:22;

then y "\/" z >> x by A2, WAYBEL_3:2;

then y "\/" z in wayabove x by WAYBEL_3:8;

then sup {y,z} in wayabove x by YELLOW_0:41;

hence sup {y,z} in the carrier of (subrelstr (wayabove x)) by YELLOW_0:def 15; :: thesis: verum

hence wayabove x is join-closed ; :: thesis: verum