let T be Noetherian sup-Semilattice; :: thesis: for I being Ideal of T holds
( ex_sup_of I,T & sup I in I )
let I be Ideal of T; :: thesis: ( ex_sup_of I,T & sup I in I )
consider a being Element of T such that
A1: a in I and
A2: for b being Element of T st b in I holds
not a < b by Def2;
A3: I is_<=_than a

proof

let d be Element of T; :: according to LATTICE3:def 9 :: thesis: ( not d in I or d <= a )
assume d in I ; :: thesis: d <= a
then a "\/" d in I by A1, WAYBEL_0:40;
then A4: not a < a "\/" d by A2;
a <= a "\/" d by YELLOW_0:22;
then a = a "\/" d by A4, ORDERS_2:def 6;
hence d <= a by YELLOW_0:22; :: thesis: verum

end;

for c being Element of T st I is_<=_than c holds
a <= c by A1;
hence ( ex_sup_of I,T & sup I in I ) by A1, A3, YELLOW_0:30; :: thesis: verum