let L be sup-Semilattice; for x being Element of L holds wayabove x is join-closed
let x be Element of L; wayabove x is join-closed
now 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))let y,
z be
Element of
L;
( 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
;
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;
verum end;
then
subrelstr (wayabove x) is join-inheriting
;
hence
wayabove x is join-closed
; verum