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

end;

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