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 ;

hence uparrow x is meet-closed ; :: thesis: verum

let x be Element of L; :: thesis: uparrow x is meet-closed

reconsider x1 = x as Element of L ;

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

inf {y,z} in the carrier of (subrelstr (uparrow x))

then
subrelstr (uparrow x) is meet-inheriting
;inf {y,z} in the carrier of (subrelstr (uparrow x))

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;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

hence uparrow x is meet-closed ; :: thesis: verum