:: deftheorem defines monotone SETLIM_1:def 1 :
for X being set
for B being SetSequence of X holds
( B is monotone iff ( not B is V56() or not B is V55() ) );