theorem Lemma154va: :: FUZIMPL4:15

for I being BinOp of [.0,1.]
for N being Fuzzy_Negation st I is satisfying_(NP) & I is N -satisfying_CP holds
( N = FNegation I & FNegation I is negation-strong )