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

proof

let x, y be Element of [.0,1.]; :: thesis: I_WB . (x,(NegationD2 . y)) = I_WB . (y,(NegationD2 . x))
x <= 1 by XXREAL_1:1;

per cases then ( x < 1 or x = 1 ) by XXREAL_0:1;

suppose F1: x < 1 ; :: thesis: I_WB . (x,(NegationD2 . y)) = I_WB . (y,(NegationD2 . x))

then F2: NegationD2 . x = 1 by FUZIMPL3:def 18;
I_WB . (x,(NegationD2 . y)) = 1 by F1, FUZIMPL1:def 22
.= I_WB . (y,(NegationD2 . x)) by F2, FUZIMPL1:8 ;
hence I_WB . (x,(NegationD2 . y)) = I_WB . (y,(NegationD2 . x)) ; :: thesis: verum

end;

suppose F1: x = 1 ; :: thesis: I_WB . (x,(NegationD2 . y)) = I_WB . (y,(NegationD2 . x))

then I_WB . (x,(NegationD2 . y)) = NegationD2 . y by FUZIMPL1:def 22
.= I_WB . (y,0) by FUZIMPL3:def 16, FUZIMPL3:27
.= I_WB . (y,(NegationD2 . x)) by F1, FUZIMPL3:def 18 ;
hence I_WB . (x,(NegationD2 . y)) = I_WB . (y,(NegationD2 . x)) ; :: thesis: verum

end;

end;

end;

hence I_WB is NegationD2 -satisfying_R-CP ; :: thesis: verum