set I = I_{0} ;

a2: ex x being Element of [.0,1.] st I_{0} . (x,x) <> 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

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

proof

SS:
1 in [.0,1.]
by XXREAL_1:1;
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;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

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

for x, y, z being Element of [.0,1.] holds I_{0} . (x,(I_{0} . (y,z))) = I_{0} . (y,(I_{0} . (x,z)))
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;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

proof

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
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;

end;( 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;

end;

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;.= 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

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;.= 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

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;.= 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

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;.= 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