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

proof

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

end;

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