let L be sup-Semilattice; :: thesis: for x being Element of L holds uparrow x is join-closed
let x be Element of L; :: thesis: uparrow x is join-closed
reconsider x1 = x as Element of L ;

now

let y, z be Element of L; :: thesis: ( y in the carrier of (subrelstr (uparrow x)) & z in the carrier of (subrelstr (uparrow x)) & ex_sup_of {y,z},L implies sup {y,z} in the carrier of (subrelstr (uparrow x)) )
assume that
A1: y in the carrier of (subrelstr (uparrow x)) and
z in the carrier of (subrelstr (uparrow x)) and
ex_sup_of {y,z},L ; :: thesis: sup {y,z} in the carrier of (subrelstr (uparrow x))
y in uparrow x by A1, YELLOW_0:def 15;
then A2: y >= x1 by WAYBEL_0:18;
y "\/" z >= y by YELLOW_0:22;
then y "\/" z >= x1 by A2, YELLOW_0:def 2;
then y "\/" z in uparrow x by WAYBEL_0:18;
then sup {y,z} in uparrow x by YELLOW_0:41;
hence sup {y,z} in the carrier of (subrelstr (uparrow x)) by YELLOW_0:def 15; :: thesis: verum

end;

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