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

proof

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

end;

hence I_KD is N_CC -satisfying_CP ; :: thesis: verum