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

proof

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

end;

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

proof

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

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

suppose D1: z = 1 ; :: thesis: I_I4 . (x,(I_I4 . (y,z))) = I_I4 . (y,(I_I4 . (x,z)))

then ( I_I4 . (y,z) = 1 & I_I4 . (x,z) = 1 ) by II4Def;
hence I_I4 . (x,(I_I4 . (y,z))) = I_I4 . (y,(I_I4 . (x,z))) by D1; :: thesis: verum

end;

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

then I_I4 . (x,(I_I4 . (y,z))) = 1 by II4Def
.= I_I4 . (y,(I_I4 . (x,z))) by f2, II4Def ;
hence I_I4 . (x,(I_I4 . (y,z))) = I_I4 . (y,(I_I4 . (x,z))) ; :: thesis: verum

end;

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

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

end;

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

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

end;

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

then F3: I_I4 . (x,z) = 1 by II4Def;
I_I4 . (x,(I_I4 . (y,z))) = 1 by II4Def, F1
.= I_I4 . (y,(I_I4 . (x,z))) by F3, II4Def ;
hence I_I4 . (x,(I_I4 . (y,z))) = I_I4 . (y,(I_I4 . (x,z))) ; :: thesis: verum

end;

end;

end;

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