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

proof

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

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

suppose F1: y = 1 ; :: thesis: I_I4 . (x,y) = I_I4 . (((FNegation I_I4) . y),((FNegation I_I4) . x))

then F2: (FNegation I_I4) . y = 0 by FUZIMPL3:def 4;
I_I4 . (x,y) = 1 by II4Def, F1
.= I_I4 . (((FNegation I_I4) . y),((FNegation I_I4) . x)) by F2, II4Def ;
hence I_I4 . (x,y) = I_I4 . (((FNegation I_I4) . y),((FNegation I_I4) . x)) ; :: thesis: verum

end;

suppose F1: x <> 1 ; :: thesis: I_I4 . (x,y) = I_I4 . (((FNegation I_I4) . y),((FNegation I_I4) . x))

then F2: (FNegation I_I4) . x = 1 by FNegD2, FUZIMPL3:def 18;
I_I4 . (x,y) = 1 by II4Def, F1
.= I_I4 . (((FNegation I_I4) . y),((FNegation I_I4) . x)) by F2, II4Def ;
hence I_I4 . (x,y) = I_I4 . (((FNegation I_I4) . y),((FNegation I_I4) . x)) ; :: thesis: verum

end;

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

then F2: (FNegation I_I4) . y = 1 by FNegD2, FUZIMPL3:def 18;
F3: ( (FNegation I_I4) . y <> 0 & (FNegation I_I4) . x = 0 ) by FNegD2, F1, FUZIMPL3:def 18;
I_I4 . (x,y) = 0 by II4Def, F1
.= I_I4 . (((FNegation I_I4) . y),((FNegation I_I4) . x)) by F3, F2, II4Def ;
hence I_I4 . (x,y) = I_I4 . (((FNegation I_I4) . y),((FNegation I_I4) . x)) ; :: thesis: verum

end;

end;

end;

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