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

proof

let x, y be Element of [.0,1.]; :: thesis: I_RS . (x,(N_CC . y)) = I_RS . (y,(N_CC . x))

per cases ( x <= N_CC . y or x > N_CC . y ) ;

suppose A1: x <= N_CC . y ; :: thesis: I_RS . (x,(N_CC . y)) = I_RS . (y,(N_CC . x))

then x <= 1 - y by FUZIMPL3:def 6;
then 1 - x >= y by XREAL_1:11;
then A2: N_CC . x >= y by FUZIMPL3:def 6;
I_RS . (x,(N_CC . y)) = 1 by A1, FUZIMPL1:def 20
.= I_RS . (y,(N_CC . x)) by A2, FUZIMPL1:def 20 ;
hence I_RS . (x,(N_CC . y)) = I_RS . (y,(N_CC . x)) ; :: thesis: verum

end;

suppose A1: x > N_CC . y ; :: thesis: I_RS . (x,(N_CC . y)) = I_RS . (y,(N_CC . x))

then x > 1 - y by FUZIMPL3:def 6;
then y > 1 - x by XREAL_1:11;
then A2: y > N_CC . x by FUZIMPL3:def 6;
I_RS . (x,(N_CC . y)) = 0 by A1, FUZIMPL1:def 20
.= I_RS . (y,(N_CC . x)) by A2, FUZIMPL1:def 20 ;
hence I_RS . (x,(N_CC . y)) = I_RS . (y,(N_CC . x)) ; :: thesis: verum

end;

end;

end;

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