theorem :: FUZIMPL4:17

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