let T be Poset; :: thesis: ( T is Mizar-widening-like implies ( T is Noetherian & T is with_suprema & T is upper-bounded ) )
assume A1: ( T is sup-Semilattice & T is Noetherian ) ; :: according to ABCMIZ_0:def 3 :: thesis: ( T is Noetherian & T is with_suprema & T is upper-bounded )
hence ( T is Noetherian & T is with_suprema ) ; :: thesis: T is upper-bounded
reconsider S = T as sup-Semilattice by A1;
the carrier of S c= the carrier of S ;
then consider a being Element of T such that
a in the carrier of T and
A2: for b being Element of T st b in the carrier of T holds
not a < b by A1, Def2;
take a ; :: according to YELLOW_0:def 5 :: thesis: the carrier of T is_<=_than a
let b be Element of T; :: according to LATTICE3:def 9 :: thesis: ( not b in the carrier of T or b <= a )
a "\/" b in the carrier of S ;
then ( a "\/" b >= a & not a < a "\/" b ) by A2, YELLOW_0:22;
then a "\/" b = a by ORDERS_2:def 10;
hence ( not b in the carrier of T or b <= a ) by A1, YELLOW_0:22; :: thesis: verum