:: deftheorem N2Def defines satisfying_(N2) FUZIMPL3:def 5 :
for N being UnOp of [.0,1.] holds
( N is satisfying_(N2) iff N is non-increasing );