let T be Poset; :: thesis: ( T is Mizar-widening-like implies ( T is Noetherian & T is with_suprema & T is upper-bounded ) )
assume that
A1: T is sup-Semilattice and
A2: T is Noetherian ; :: according to ABCMIZ_0:def 3 :: thesis: ( T is Noetherian & T is with_suprema & 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
A3: for b being Element of T st b in the carrier of T holds
not a < b by A2, Def2;
thus ( T is Noetherian & T is with_suprema ) by A1, A2; :: thesis: T is upper-bounded
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 )
A4: a "\/" b in the carrier of S ;
then A5: a "\/" b >= a by YELLOW_0:22;
not a < a "\/" b by A3, A4;
then a "\/" b = a by A5, ORDERS_2:def 6;
hence ( not b in the carrier of T or b <= a ) by A1, YELLOW_0:22; :: thesis: verum