let I be BinOp of [.0,1.]; :: thesis: for N being negation-strong Fuzzy_Negation st I is N -satisfying_R-CP holds
I is N -satisfying_CP
let N be negation-strong Fuzzy_Negation; :: thesis: ( I is N -satisfying_R-CP implies I is N -satisfying_CP )
assume a0: I is N -satisfying_R-CP ; :: thesis: I is N -satisfying_CP
d1: N is involutive by FUZIMPL3:def 11, FUZIMPL3:def 13;
for x, y being Element of [.0,1.] holds I . (x,y) = I . ((N . y),(N . x))

proof

let x, y be Element of [.0,1.]; :: thesis: I . (x,y) = I . ((N . y),(N . x))
I . (x,y) = I . (x,(N . (N . y))) by d1, FUZIMPL3:def 8
.= I . ((N . y),(N . x)) by a0 ;
hence I . (x,y) = I . ((N . y),(N . x)) ; :: thesis: verum

end;

hence I is N -satisfying_CP ; :: thesis: verum