theorem :: WAYBEL_0:64
for L being sup-Semilattice
for X being non empty lower Subset of L holds
( X is Ideal of L iff subrelstr X is join-inheriting )