let L be Semilattice; :: thesis: for x being Element of L holds waybelow x is meet-closed
let x be Element of L; :: thesis: waybelow x is meet-closed

now :: thesis: for y, z being Element of L st y in the carrier of (subrelstr (waybelow x)) & z in the carrier of (subrelstr (waybelow x)) & ex_inf_of {y,z},L holds
inf {y,z} in the carrier of (subrelstr (waybelow x))

let y, z be Element of L; :: thesis: ( y in the carrier of (subrelstr (waybelow x)) & z in the carrier of (subrelstr (waybelow x)) & ex_inf_of {y,z},L implies inf {y,z} in the carrier of (subrelstr (waybelow x)) )
assume that
A1: y in the carrier of (subrelstr (waybelow x)) and
z in the carrier of (subrelstr (waybelow x)) and
ex_inf_of {y,z},L ; :: thesis: inf {y,z} in the carrier of (subrelstr (waybelow x))
y in waybelow x by A1, YELLOW_0:def 15;
then A2: y << x by WAYBEL_3:7;
y "/\" z <= y by YELLOW_0:23;
then y "/\" z << x by A2, WAYBEL_3:2;
then y "/\" z in waybelow x by WAYBEL_3:7;
then inf {y,z} in waybelow x by YELLOW_0:40;
hence inf {y,z} in the carrier of (subrelstr (waybelow x)) by YELLOW_0:def 15; :: thesis: verum

end;

then subrelstr (waybelow x) is meet-inheriting ;
hence waybelow x is meet-closed ; :: thesis: verum