set N = N_CC ;
set I = I_KD ;
for x, y being Element of [.0,1.] holds I_KD . (x,(N_CC . y)) = I_KD . (y,(N_CC . x))

proof

let x, y be Element of [.0,1.]; :: thesis: I_KD . (x,(N_CC . y)) = I_KD . (y,(N_CC . x))
I_KD . (x,(N_CC . y)) = max ((1 - x),(N_CC . y)) by FUZIMPL1:def 18
.= max ((1 - x),(1 - y)) by FUZIMPL3:def 6
.= max ((1 - y),(N_CC . x)) by FUZIMPL3:def 6
.= I_KD . (y,(N_CC . x)) by FUZIMPL1:def 18 ;
hence I_KD . (x,(N_CC . y)) = I_KD . (y,(N_CC . x)) ; :: thesis: verum

end;

hence I_KD is N_CC -satisfying_R-CP ; :: thesis: verum