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

proof

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

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

suppose F1: x = 0 ; :: thesis: I_GD . (x,(NegationD1 . y)) = I_GD . (y,(NegationD1 . x))

then x <= NegationD1 . y by XXREAL_1:1;
then I_GD . (x,(NegationD1 . y)) = 1 by FUZIMPL1:def 16
.= I_GD . (y,1) by FUZIMPL1:8
.= I_GD . (y,(NegationD1 . x)) by F1, FUZIMPL3:def 4 ;
hence I_GD . (x,(NegationD1 . y)) = I_GD . (y,(NegationD1 . x)) ; :: thesis: verum

end;

suppose F1: ( x <> 0 & y = 0 ) ; :: thesis: I_GD . (x,(NegationD1 . y)) = I_GD . (y,(NegationD1 . x))

then F2: ( NegationD1 . x = 0 & NegationD1 . y = 1 ) by FUZIMPL3:def 17;
I_GD . (x,(NegationD1 . y)) = 1 by F2, FUZIMPL1:8
.= I_GD . (y,(NegationD1 . x)) by F1, F2, FUZIMPL1:def 3 ;
hence I_GD . (x,(NegationD1 . y)) = I_GD . (y,(NegationD1 . x)) ; :: thesis: verum

end;

suppose F1: ( x <> 0 & y <> 0 ) ; :: thesis: I_GD . (x,(NegationD1 . y)) = I_GD . (y,(NegationD1 . x))

then F2: ( NegationD1 . x = 0 & NegationD1 . y = 0 ) by FUZIMPL3:def 17;
F4: y > 0 by F1, XXREAL_1:1;
x > NegationD1 . y by F1, F2, XXREAL_1:1;
then I_GD . (x,(NegationD1 . y)) = NegationD1 . y by FUZIMPL1:def 16
.= I_GD . (y,(NegationD1 . x)) by F2, F4, FUZIMPL1:def 16 ;
hence I_GD . (x,(NegationD1 . y)) = I_GD . (y,(NegationD1 . x)) ; :: thesis: verum

end;

end;

end;

hence I_GD is NegationD1 -satisfying_R-CP ; :: thesis: verum