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

proof

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

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

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

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

end;

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

then x < 1 - y by FUZIMPL3:def 6;
then y < 1 - x by XREAL_1:12;
then A2: y < N_CC . x by FUZIMPL3:def 6;
A3: ( N_CC . x = 1 - x & N_CC . y = 1 - y ) by FUZIMPL3:def 6;
I_FD . ((N_CC . x),y) = max ((1 - (N_CC . x)),y) by A2, FUZIMPL1:def 23
.= max ((1 - (N_CC . y)),x) by A3
.= I_FD . ((N_CC . y),x) by A1, FUZIMPL1:def 23 ;
hence I_FD . ((N_CC . x),y) = I_FD . ((N_CC . y),x) ; :: thesis: verum

end;

end;

end;

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