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

proof

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

end;

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