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

proof

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

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

suppose F1: x = 0 ; :: thesis: I_I3 . (x,y) = I_I3 . (((FNegation I_I3) . y),((FNegation I_I3) . x))

F3: 1 in [.0,1.] by XXREAL_1:1;
thus I_I3 . (x,y) = 1 by II3Def, F1
.= I_I3 . (((FNegation I_I3) . y),1) by II3Def, F3
.= I_I3 . (((FNegation I_I3) . y),((FNegation I_I3) . x)) by F1, FUZIMPL3:def 4 ; :: thesis: verum

end;

suppose F1: y <> 0 ; :: thesis: I_I3 . (x,y) = I_I3 . (((FNegation I_I3) . y),((FNegation I_I3) . x))

then F2: (FNegation I_I3) . y = 0 by FNegI3, FUZIMPL3:def 17;
thus I_I3 . (x,y) = 1 by II3Def, F1
.= I_I3 . (((FNegation I_I3) . y),((FNegation I_I3) . x)) by F2, II3Def ; :: thesis: verum

end;

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

then F3: ( (FNegation I_I3) . y <> 0 & (FNegation I_I3) . x = 0 ) by FNegI3, FUZIMPL3:def 17;
thus I_I3 . (x,y) = 0 by II3Def, F1
.= I_I3 . (((FNegation I_I3) . y),((FNegation I_I3) . x)) by F3, II3Def ; :: thesis: verum

end;

end;

end;

hence I_I3 is FNegation I_I3 -satisfying_CP ; :: thesis: verum