:: deftheorem defines Mizar-widening-like ABCMIZ_0:def 3 :
for T being Poset holds
( T is Mizar-widening-like iff ( T is sup-Semilattice & T is Noetherian ) );