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))
z in uparrow x by A2, YELLOW_0:def 15;
then A3: z >= x1 by WAYBEL_0:18;
y in uparrow x by A1, YELLOW_0:def 15;
then y >= x1 by WAYBEL_0:18;
then y "/\" z >= x1 "/\" x1 by A3, 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