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

proof

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

end;

hence I is N -satisfying_R-CP ; :: thesis: verum