let L be Semilattice; :: thesis: 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; :: thesis: ( 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 :: thesis: ( subrelstr X is meet-inheriting implies X is Filter of L )
assume A2:
X is
Filter of
L
;
:: thesis: subrelstr X is meet-inheriting thus
subrelstr X is
meet-inheriting
:: thesis: verumproof
let x,
y be
Element of
L;
:: according to YELLOW_0:def 16 :: thesis: ( 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 A3:
(
x in the
carrier of
(subrelstr X) &
y in the
carrier of
(subrelstr X) &
ex_inf_of {x,y},
L )
;
:: thesis: "/\" {x,y},L in the carrier of (subrelstr X)
then consider z being
Element of
L such that A4:
(
z in X &
x >= z &
y >= z )
by A1, A2, Def2;
z is_<=_than {x,y}
by A4, YELLOW_0:8;
then
z <= inf {x,y}
by A3, YELLOW_0:def 10;
hence
"/\" {x,y},
L in the
carrier of
(subrelstr X)
by A1, A4, Def20;
:: thesis: verum
end;
end;
assume A5:
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)
; :: according to YELLOW_0:def 16 :: thesis: X is Filter of L
X is filtered
hence
X is Filter of L
; :: thesis: verum