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

proof

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

per cases ( ( x > 0 & y > 0 ) or ( x = 0 & y > 0 ) or ( x > 0 & y = 0 ) or ( x = 0 & y = 0 ) ) by XXREAL_1:1;

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

then F2: ( NegationD1 . x = 0 & NegationD1 . y = 0 ) by FUZIMPL3:def 17;
I_YG . (x,(NegationD1 . y)) = (NegationD1 . y) to_power x by F1, FUZIMPL1:def 21
.= 0 by F1, F2, POWER:def 2
.= 0 to_power y by F1, POWER:def 2
.= (NegationD1 . x) to_power y by F1, FUZIMPL3:def 17
.= I_YG . (y,(NegationD1 . x)) by F1, FUZIMPL1:def 21 ;
hence I_YG . (x,(NegationD1 . y)) = I_YG . (y,(NegationD1 . x)) ; :: thesis: verum

end;

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

then ( NegationD1 . x = 1 & NegationD1 . y = 0 ) by FUZIMPL3:def 17;
then I_YG . (x,(NegationD1 . y)) = 1 by F1, FUZIMPL1:def 21
.= 1 to_power y by POWER:26
.= (NegationD1 . x) to_power y by F1, FUZIMPL3:def 17
.= I_YG . (y,(NegationD1 . x)) by FUZIMPL1:def 21, F1 ;
hence I_YG . (x,(NegationD1 . y)) = I_YG . (y,(NegationD1 . x)) ; :: thesis: verum

end;

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

then F2: ( NegationD1 . x = 0 & NegationD1 . y = 1 ) by FUZIMPL3:def 17;
I_YG . (x,(NegationD1 . y)) = (NegationD1 . y) to_power x by F1, FUZIMPL1:def 21
.= 1 by F2, POWER:26
.= I_YG . (y,(NegationD1 . x)) by F1, F2, FUZIMPL1:def 21 ;
hence I_YG . (x,(NegationD1 . y)) = I_YG . (y,(NegationD1 . x)) ; :: thesis: verum

end;

suppose ( x = 0 & y = 0 ) ; :: thesis: I_YG . (x,(NegationD1 . y)) = I_YG . (y,(NegationD1 . x))

then F2: ( NegationD1 . x = 1 & NegationD1 . y = 1 ) by FUZIMPL3:def 17;
then I_YG . (x,(NegationD1 . y)) = (NegationD1 . y) to_power x by FUZIMPL1:def 21
.= 1 by F2, POWER:26
.= (NegationD1 . x) to_power y by F2, POWER:26
.= I_YG . (y,(NegationD1 . x)) by FUZIMPL1:def 21, F2 ;
hence I_YG . (x,(NegationD1 . y)) = I_YG . (y,(NegationD1 . x)) ; :: thesis: verum

end;

end;

end;

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