set I = I_{1} ;

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

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

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

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

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

proof

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

( 0 <= x & x <= 1 ) by XXREAL_1:1;

end;( 0 <= x & x <= 1 ) by XXREAL_1:1;

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

proof

then A3:
not I_{1} is satisfying_(NP)
;
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;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

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

then
I_{1} is satisfying_(EP)
;
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;

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

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

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

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

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

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;hence I_{1} . (x,(I_{1} . (y,z))) = I_{1} . (y,(I_{1} . (x,z))) by B1, FUZIMPL1:def 25; :: thesis: verum

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

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

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