let L be Semilattice; for X being non empty upper Subset of L holds
( X is Filter of L iff subrelstr X is meet-inheriting )
let X be non empty upper Subset of L; ( X is Filter of L iff subrelstr X is meet-inheriting )
set S = subrelstr X;
A1:
the carrier of (subrelstr X) = X
by YELLOW_0:def 15;
hereby ( subrelstr X is meet-inheriting implies X is Filter of L )
assume A2:
X is
Filter of
L
;
subrelstr X is meet-inheriting thus
subrelstr X is
meet-inheriting
verumproof
let x,
y be
Element of
L;
YELLOW_0:def 16 ( not x in the carrier of (subrelstr X) or not y in the carrier of (subrelstr X) or not ex_inf_of {x,y},L or "/\" ({x,y},L) in the carrier of (subrelstr X) )
assume that A3:
x in the
carrier of
(subrelstr X)
and A4:
y in the
carrier of
(subrelstr X)
and A5:
ex_inf_of {x,y},
L
;
"/\" ({x,y},L) in the carrier of (subrelstr X)
consider z being
Element of
L such that A6:
z in X
and A7:
x >= z
and A8:
y >= z
by A1, A2, A3, A4, Def2;
z is_<=_than {x,y}
by A7, A8, YELLOW_0:8;
then
z <= inf {x,y}
by A5, YELLOW_0:def 10;
hence
"/\" (
{x,y},
L)
in the
carrier of
(subrelstr X)
by A1, A6, Def20;
verum
end;
end;
assume A9:
for x, y being Element of L st x in the carrier of (subrelstr X) & y in the carrier of (subrelstr X) & ex_inf_of {x,y},L holds
inf {x,y} in the carrier of (subrelstr X)
; YELLOW_0:def 16 X is Filter of L
X is filtered
hence
X is Filter of L
; verum