set I = I_I3 ;
ex y being Element of [.0,1.] st I_I3 . (1,y) <> y

proof

reconsider y = 1 / 2 as Element of [.0,1.] by XXREAL_1:1;
take y ; :: thesis: I_I3 . (1,y) <> y
1 in [.0,1.] by XXREAL_1:1;
hence I_I3 . (1,y) <> y by II3Def; :: thesis: verum

end;

then T1: not I_I3 is satisfying_(NP) by FUZIMPL2:def 1;
for x, y, z being Element of [.0,1.] holds I_I3 . (x,(I_I3 . (y,z))) = I_I3 . (y,(I_I3 . (x,z)))

proof

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

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

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

then D2: ( I_I3 . (y,z) = 1 & I_I3 . (x,z) = 1 ) by II3Def;
then I_I3 . (x,(I_I3 . (y,z))) = 1 by II3Def
.= I_I3 . (y,(I_I3 . (x,z))) by II3Def, D2 ;
hence I_I3 . (x,(I_I3 . (y,z))) = I_I3 . (y,(I_I3 . (x,z))) ; :: thesis: verum

end;

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

then ( I_I3 . (y,z) = 0 & I_I3 . (x,z) = 0 ) by II3Def;
hence I_I3 . (x,(I_I3 . (y,z))) = I_I3 . (y,(I_I3 . (x,z))) by F1; :: thesis: verum

end;

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

then ( I_I3 . (y,z) = 0 & I_I3 . (x,z) = 1 ) by II3Def;
hence I_I3 . (x,(I_I3 . (y,z))) = I_I3 . (y,(I_I3 . (x,z))) by F1, II3Def; :: thesis: verum

end;

suppose ( z = 0 & y = 0 & x = 0 ) ; :: thesis: I_I3 . (x,(I_I3 . (y,z))) = I_I3 . (y,(I_I3 . (x,z)))

hence I_I3 . (x,(I_I3 . (y,z))) = I_I3 . (y,(I_I3 . (x,z))) ; :: thesis: verum

end;

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

then I_I3 . (y,z) = 1 by II3Def;
then I_I3 . (x,(I_I3 . (y,z))) = 1 by II3Def
.= I_I3 . (y,(I_I3 . (x,z))) by F1, II3Def ;
hence I_I3 . (x,(I_I3 . (y,z))) = I_I3 . (y,(I_I3 . (x,z))) ; :: thesis: verum

end;

end;

end;

hence ( I_I3 is satisfying_(EP) & not I_I3 is satisfying_(NP) ) by T1, FUZIMPL2:def 2; :: thesis: verum