:: deftheorem defines negation-strict FUZIMPL3:def 12 :
for N being UnOp of [.0,1.] holds
( N is negation-strict iff ( N is satisfying_(N3) & N is satisfying_(N4) ) );