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

proof

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

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

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

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

end;

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

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

end;

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

then F2: ( NegationD1 . x = 0 & NegationD1 . y = 0 ) by FUZIMPL3:def 17;
F3: 0 in [.0,1.] by XXREAL_1:1;
F4: y > 0 by F1, XXREAL_1:1;
x > NegationD1 . y by F1, F2, XXREAL_1:1;
then I_GG . (x,(NegationD1 . y)) = (NegationD1 . y) / x by FUZIMPL1:def 19
.= 0 / y by F2
.= I_GG . (y,0) by F3, F4, FUZIMPL1:def 19
.= I_GG . (y,(NegationD1 . x)) by F1, FUZIMPL3:def 17 ;
hence I_GG . (x,(NegationD1 . y)) = I_GG . (y,(NegationD1 . x)) ; :: thesis: verum

end;

end;

end;

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