let L be sup-Semilattice; :: thesis: for S being non empty lower Subset of L holds
( S is Ideal of L iff S is join-closed )
let S be non empty lower Subset of L; :: thesis: ( S is Ideal of L iff S is join-closed )
( S is Ideal of L iff subrelstr S is join-inheriting ) by WAYBEL_0:64;
hence ( S is Ideal of L iff S is join-closed ) by Def2; :: thesis: verum