theorem :: FUZIMPL4:22

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