set I = I_{1} ;
a2: for x being Element of [.0,1.] holds I_{1} . (x,x) = 1

proof

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

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

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

hence I_{1} . (x,x) = 1 by FUZIMPL1:def 25; :: thesis: verum

end;

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

hence I_{1} . (x,x) = 1 by FUZIMPL1:def 25; :: thesis: verum

end;

suppose x = 1 ; :: thesis: I_{1} . (x,x) = 1

hence I_{1} . (x,x) = 1 by FUZIMPL1:def 25; :: thesis: verum

end;

end;

end;

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

proof

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

end;

then A3: not I_{1} is satisfying_(NP) ;
for x, y, z being Element of [.0,1.] holds I_{1} . (x,(I_{1} . (y,z))) = I_{1} . (y,(I_{1} . (x,z)))

proof

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

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

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

then I_{1} . (y,(I_{1} . (x,z))) = 1 by FUZIMPL1:def 25;
hence I_{1} . (x,(I_{1} . (y,z))) = I_{1} . (y,(I_{1} . (x,z))) by FUZIMPL1:def 25, F1; :: thesis: verum

end;

end;

end;

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