let L be sup-Semilattice; :: thesis: 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; :: thesis: ( 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 :: thesis: ( subrelstr X is join-inheriting implies X is Ideal of L )
assume A2:
X is
Ideal of
L
;
:: thesis: subrelstr X is join-inheriting thus
subrelstr X is
join-inheriting
:: thesis: verumproof
let x,
y be
Element of
L;
:: according to YELLOW_0:def 17 :: thesis: ( 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 A3:
(
x in the
carrier of
(subrelstr X) &
y in the
carrier of
(subrelstr X) &
ex_sup_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, Def1;
z is_>=_than {x,y}
by A4, YELLOW_0:8;
then
z >= sup {x,y}
by A3, YELLOW_0:def 9;
hence
"\/" {x,y},
L in the
carrier of
(subrelstr X)
by A1, A4, Def19;
:: 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_sup_of {x,y},L holds
sup {x,y} in the carrier of (subrelstr X)
; :: according to YELLOW_0:def 17 :: thesis: X is Ideal of L
X is directed
hence
X is Ideal of L
; :: thesis: verum