let L be Semilattice; :: thesis: for x being Element of L holds uparrow x is meet-closed
let x be Element of L; :: thesis: uparrow x is meet-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_inf_of {y,z},L implies inf {y,z} in the carrier of (subrelstr (uparrow x)) )
assume that
A1: y in the carrier of (subrelstr (uparrow x)) and
A2: z in the carrier of (subrelstr (uparrow x)) and
ex_inf_of {y,z},L ; :: thesis: inf {y,z} in the carrier of (subrelstr (uparrow x))
( y in uparrow x & z in uparrow x ) by A1, A2, YELLOW_0:def 15;
then ( y >= x1 & z >= x1 ) by WAYBEL_0:18;
then y "/\" z >= x1 "/\" x1 by YELLOW_3:2;
then y "/\" z >= x1 by YELLOW_5:2;
then y "/\" z in uparrow x by WAYBEL_0:18;
then inf {y,z} in uparrow x by YELLOW_0:40;
hence inf {y,z} in the carrier of (subrelstr (uparrow x)) by YELLOW_0:def 15; :: thesis: verum

end;

then subrelstr (uparrow x) is meet-inheriting by YELLOW_0:def 16;
hence uparrow x is meet-closed by Def1; :: thesis: verum