:: deftheorem defines satisfying_(N3) FUZIMPL3:def 9 :
for N being UnOp of [.0,1.] holds
( N is satisfying_(N3) iff N is decreasing );