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

proof

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

end;

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