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

proof

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

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

suppose A1: x <= N_CC . y ; :: thesis: I_FD . (x,(N_CC . y)) = I_FD . (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_FD . (x,(N_CC . y)) = 1 by A1, FUZIMPL1:def 23
.= I_FD . (y,(N_CC . x)) by A2, FUZIMPL1:def 23 ;
hence I_FD . (x,(N_CC . y)) = I_FD . (y,(N_CC . x)) ; :: thesis: verum

end;

suppose A1: x > N_CC . y ; :: thesis: I_FD . (x,(N_CC . y)) = I_FD . (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_FD . (x,(N_CC . y)) = max ((1 - x),(N_CC . y)) by A1, FUZIMPL1:def 23
.= max ((1 - x),(1 - y)) by FUZIMPL3:def 6
.= max ((1 - y),(N_CC . x)) by FUZIMPL3:def 6
.= I_FD . (y,(N_CC . x)) by A2, FUZIMPL1:def 23 ;
hence I_FD . (x,(N_CC . y)) = I_FD . (y,(N_CC . x)) ; :: thesis: verum

end;

end;

end;

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