theorem Th1: :: ABCMIZ_0:1

for T being Noetherian sup-Semilattice
for I being Ideal of T holds
( ex_sup_of I,T & sup I in I )