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