let L be Semilattice; for x being Element of L holds uparrow x is meet-closed
let x be Element of L; uparrow x is meet-closed
reconsider x1 = x as Element of L ;
now 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))let y,
z be
Element of
L;
( 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
;
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;
verum end;
then
subrelstr (uparrow x) is meet-inheriting
;
hence
uparrow x is meet-closed
; verum