let L be Semilattice; for x being Element of L holds downarrow x is meet-closed
let x be Element of L; downarrow 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 (downarrow x)) & z in the carrier of (subrelstr (downarrow x)) & ex_inf_of {y,z},L holds
inf {y,z} in the carrier of (subrelstr (downarrow x))let y,
z be
Element of
L;
( 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
;
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;
verum end;
then
subrelstr (downarrow x) is meet-inheriting
;
hence
downarrow x is meet-closed
; verum