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

proof

let x, y be Element of [.0,1.]; :: thesis: I_RC . ((N_CC . x),y) = I_RC . ((N_CC . y),x)
SA: N_CC . x = 1 - x by FUZIMPL3:def 6;
SB: N_CC . y = 1 - y by FUZIMPL3:def 6;
I_RC . ((N_CC . x),y) = (1 - (N_CC . x)) + ((N_CC . x) * y) by FUZIMPL1:def 17
.= (1 - (N_CC . y)) + ((N_CC . y) * x) by SA, SB
.= I_RC . ((N_CC . y),x) by FUZIMPL1:def 17 ;
hence I_RC . ((N_CC . x),y) = I_RC . ((N_CC . y),x) ; :: thesis: verum

end;

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