:: deftheorem defines negation-strong FUZIMPL3:def 13 :
for N being UnOp of [.0,1.] holds
( N is negation-strong iff N is satisfying_(N5) );