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

proof

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

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

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

end;

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

end;

end;

end;

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