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

proof

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

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

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

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

end;

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

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

end;

end;

end;

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