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

proof

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

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

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

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

end;

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

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

end;

end;

end;

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