:: deftheorem Def9 defines monotoneclass PROB_3:def 11 :
for Omega being non empty set
for X being Subset-Family of Omega
for b₃ being MonotoneClass of Omega holds
( b₃ = monotoneclass X iff ( X c= b₃ & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds
b₃ c= Z ) ) );