set I = I_{0} ;
a2: ex x being Element of [.0,1.] st I_{0} . (x,x) <> 1

proof

reconsider x = 1 / 2 as Element of [.0,1.] by XXREAL_1:1;
I_{0} . (x,x) = 0 by FUZIMPL1:def 24;
hence ex x being Element of [.0,1.] st I_{0} . (x,x) <> 1 ; :: thesis: verum

end;

SS: 1 in [.0,1.] by XXREAL_1:1;
SA: 0 in [.0,1.] by XXREAL_1:1;
a3: not for y being Element of [.0,1.] holds I_{0} . (1,y) = y

proof

reconsider y = 1 / 2 as Element of [.0,1.] by XXREAL_1:1;
I_{0} . (1,y) = 0 by FUZIMPL1:def 24, SS;
hence not for y being Element of [.0,1.] holds I_{0} . (1,y) = y ; :: thesis: verum

end;

for x, y, z being Element of [.0,1.] holds I_{0} . (x,(I_{0} . (y,z))) = I_{0} . (y,(I_{0} . (x,z)))

proof

let x, y, z be Element of [.0,1.]; :: thesis: I_{0} . (x,(I_{0} . (y,z))) = I_{0} . (y,(I_{0} . (x,z)))
( x >= 0 & y >= 0 & z <= 1 ) by XXREAL_1:1;

per cases then ( z = 1 or x = 0 or y = 0 or ( x > 0 & z < 1 & y > 0 ) ) by XXREAL_0:1;

suppose B1: z = 1 ; :: thesis: I_{0} . (x,(I_{0} . (y,z))) = I_{0} . (y,(I_{0} . (x,z)))

then B2: I_{0} . (x,(I_{0} . (y,z))) = I_{0} . (x,1) by FUZIMPL1:def 24
.= 1 by FUZIMPL1:def 24, SS ;
I_{0} . (y,(I_{0} . (x,z))) = I_{0} . (y,1) by FUZIMPL1:def 24, B1
.= 1 by FUZIMPL1:def 24, SS ;
hence I_{0} . (x,(I_{0} . (y,z))) = I_{0} . (y,(I_{0} . (x,z))) by B2; :: thesis: verum

end;

suppose B1: x = 0 ; :: thesis: I_{0} . (x,(I_{0} . (y,z))) = I_{0} . (y,(I_{0} . (x,z)))

then I_{0} . (y,(I_{0} . (x,z))) = I_{0} . (y,1) by FUZIMPL1:def 24
.= 1 by FUZIMPL1:def 24, SS ;
hence I_{0} . (x,(I_{0} . (y,z))) = I_{0} . (y,(I_{0} . (x,z))) by B1, FUZIMPL1:def 24; :: thesis: verum

end;

suppose B1: y = 0 ; :: thesis: I_{0} . (x,(I_{0} . (y,z))) = I_{0} . (y,(I_{0} . (x,z)))

then I_{0} . (x,(I_{0} . (y,z))) = I_{0} . (x,1) by FUZIMPL1:def 24
.= 1 by FUZIMPL1:def 24, SS ;
hence I_{0} . (x,(I_{0} . (y,z))) = I_{0} . (y,(I_{0} . (x,z))) by B1, FUZIMPL1:def 24; :: thesis: verum

end;

suppose F1: ( x > 0 & z < 1 & y > 0 ) ; :: thesis: I_{0} . (x,(I_{0} . (y,z))) = I_{0} . (y,(I_{0} . (x,z)))

then F2: I_{0} . (y,(I_{0} . (x,z))) = I_{0} . (y,0) by FUZIMPL1:def 24
.= 0 by SA, F1, FUZIMPL1:def 24 ;
I_{0} . (x,(I_{0} . (y,z))) = I_{0} . (x,0) by F1, FUZIMPL1:def 24
.= 0 by SA, FUZIMPL1:def 24, F1 ;
hence I_{0} . (x,(I_{0} . (y,z))) = I_{0} . (y,(I_{0} . (x,z))) by F2; :: thesis: verum

end;

end;

end;

hence ( not I_{0} is satisfying_(NP) & I_{0} is satisfying_(EP) & not I_{0} is satisfying_(IP) & not I_{0} is satisfying_(OP) ) by a2, a3; :: thesis: verum