set I = I_RC ;
I0:
1 / 2 in [.0,1.]
by XXREAL_1:1;
then p1: I_RC . ((1 / 2),(1 / 2)) =
(1 - (1 / 2)) + ((1 / 2) * (1 / 2))
by FUZIMPL1:def 17
.=
3 / 4
;
at:
for y being Element of [.0,1.] holds I_RC . (1,y) = y
for x, y, z being Element of [.0,1.] holds I_RC . (x,(I_RC . (y,z))) = I_RC . (y,(I_RC . (x,z)))
proof
let x,
y,
z be
Element of
[.0,1.];
I_RC . (x,(I_RC . (y,z))) = I_RC . (y,(I_RC . (x,z)))
i0:
I_RC . (
y,
z)
= (1 - y) + (y * z)
by FUZIMPL1:def 17;
i2:
I_RC . (
x,
z)
= (1 - x) + (x * z)
by FUZIMPL1:def 17;
I1:
I_RC . (
x,
(I_RC . (y,z)))
= (1 - x) + (x * ((1 - y) + (y * z)))
by i0, FUZIMPL1:def 17;
I_RC . (
y,
(I_RC . (x,z)))
= (1 - y) + (y * ((1 - x) + (x * z)))
by i2, FUZIMPL1:def 17;
hence
I_RC . (
x,
(I_RC . (y,z)))
= I_RC . (
y,
(I_RC . (x,z)))
by I1;
verum
end;
hence
( I_RC is satisfying_(NP) & I_RC is satisfying_(EP) & not I_RC is satisfying_(IP) & not I_RC is satisfying_(OP) )
by at, p1, I0; verum