theorem :: FUZIMPL4:23

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