set I = I_{0} ;
a2:
ex x being Element of [.0,1.] st I_{0} . (x,x) <> 1
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
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.];
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
;
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;
verum end; suppose F1:
(
x > 0 &
z < 1 &
y > 0 )
;
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;
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; verum