let L be sup-Semilattice; for X being non empty lower Subset of L holds
( X is Ideal of L iff subrelstr X is join-inheriting )
let X be non empty lower Subset of L; ( X is Ideal of L iff subrelstr X is join-inheriting )
set S = subrelstr X;
A1:
the carrier of (subrelstr X) = X
by YELLOW_0:def 15;
hereby ( subrelstr X is join-inheriting implies X is Ideal of L )
assume A2:
X is
Ideal of
L
;
subrelstr X is join-inheriting thus
subrelstr X is
join-inheriting
verumproof
let x,
y be
Element of
L;
YELLOW_0:def 17 ( not x in the carrier of (subrelstr X) or not y in the carrier of (subrelstr X) or not ex_sup_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_sup_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, Def1;
z is_>=_than {x,y}
by A7, A8, YELLOW_0:8;
then
z >= sup {x,y}
by A5, YELLOW_0:def 9;
hence
"\/" (
{x,y},
L)
in the
carrier of
(subrelstr X)
by A1, A6, Def19;
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_sup_of {x,y},L holds
sup {x,y} in the carrier of (subrelstr X)
; YELLOW_0:def 17 X is Ideal of L
X is directed
hence
X is Ideal of L
; verum