let I be BinOp of [.0,1.]; :: thesis: for N being negation-strong Fuzzy_Negation st N = FNegation I & I is satisfying_(EP) holds
( I is satisfying_(I3) & I is satisfying_(I4) & I is satisfying_(I5) & I is satisfying_(NP) & I is N -satisfying_CP )
let N be negation-strong Fuzzy_Negation; :: thesis: ( N = FNegation I & I is satisfying_(EP) implies ( I is satisfying_(I3) & I is satisfying_(I4) & I is satisfying_(I5) & I is satisfying_(NP) & I is N -satisfying_CP ) )
assume A0: N = FNegation I ; :: thesis: ( not I is satisfying_(EP) or ( I is satisfying_(I3) & I is satisfying_(I4) & I is satisfying_(I5) & I is satisfying_(NP) & I is N -satisfying_CP ) )
assume A1: I is satisfying_(EP) ; :: thesis: ( I is satisfying_(I3) & I is satisfying_(I4) & I is satisfying_(I5) & I is satisfying_(NP) & I is N -satisfying_CP )
A2: N is involutive by FUZIMPL3:def 13, FUZIMPL3:def 11;
for x, y being Element of [.0,1.] holds I . ((N . y),(N . x)) = I . (x,y)

proof

let x, y be Element of [.0,1.]; :: thesis: I . ((N . y),(N . x)) = I . (x,y)
ZZ: ( N . y in [.0,1.] & 0 in [.0,1.] ) by XXREAL_1:1;
I . ((N . y),(N . x)) = I . ((N . y),(I . (x,0))) by A0, FUZIMPL3:def 16
.= I . (x,(I . ((N . y),0))) by A1, FUZIMPL2:def 2, ZZ
.= I . (x,(N . (N . y))) by FUZIMPL3:def 16, A0
.= I . (x,y) by A2, FUZIMPL3:def 8 ;
hence I . ((N . y),(N . x)) = I . (x,y) ; :: thesis: verum

end;

then T1: I is N -satisfying_CP ;
then I is satisfying_(NP) by A0, Lemma156i;
hence ( I is satisfying_(I3) & I is satisfying_(I4) & I is satisfying_(I5) & I is satisfying_(NP) & I is N -satisfying_CP ) by T1, Lemma154vb; :: thesis: verum