let I be BinOp of [.0,1.]; :: thesis: 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 )
let N be Fuzzy_Negation; :: thesis: ( I is N -satisfying_CP & I is satisfying_(I1) & I is satisfying_(NP) implies ( I in FI & FNegation I = N & N is negation-strong ) )
assume A1: ( I is N -satisfying_CP & I is satisfying_(I1) & I is satisfying_(NP) ) ; :: thesis: ( I in FI & FNegation I = N & N is negation-strong )
A4: I is satisfying_(I2) by A1, Corr157i;
I is satisfying_(I3) by A1, Lemma154vb;
hence I in FI by A1, A4, FUZIMPL1:def 15; :: thesis: ( FNegation I = N & N is negation-strong )
thus FNegation I = N by A1, Lemma154va; :: thesis: N is negation-strong
hence N is negation-strong by A1, Lemma154va; :: thesis: verum