set I = I_KD ;
K1:
( 1 in [.0,1.] & 1 / 2 in [.0,1.] )
by XXREAL_1:1;
ka:
for y being Element of [.0,1.] holds I_KD . (1,y) = y
n1: I_KD . ((1 / 2),(1 / 2)) =
max ((1 - (1 / 2)),(1 / 2))
by FUZIMPL1:def 18, K1
.=
max ((1 / 2),(1 / 2))
;
for x, y, z being Element of [.0,1.] holds I_KD . (x,(I_KD . (y,z))) = I_KD . (y,(I_KD . (x,z)))
proof
let x,
y,
z be
Element of
[.0,1.];
I_KD . (x,(I_KD . (y,z))) = I_KD . (y,(I_KD . (x,z)))
y2:
I_KD . (
y,
z)
= max (
(1 - y),
z)
by FUZIMPL1:def 18;
y3:
I_KD . (
x,
z)
= max (
(1 - x),
z)
by FUZIMPL1:def 18;
Y1:
I_KD . (
x,
(I_KD . (y,z))) =
max (
(1 - x),
(max ((1 - y),z)))
by y2, FUZIMPL1:def 18
.=
max (
(max ((1 - x),(1 - y))),
z)
by XXREAL_0:34
;
I_KD . (
y,
(I_KD . (x,z))) =
max (
(1 - y),
(max ((1 - x),z)))
by y3, FUZIMPL1:def 18
.=
max (
(max ((1 - y),(1 - x))),
z)
by XXREAL_0:34
;
hence
I_KD . (
x,
(I_KD . (y,z)))
= I_KD . (
y,
(I_KD . (x,z)))
by Y1;
verum
end;
hence
( I_KD is satisfying_(NP) & I_KD is satisfying_(EP) & not I_KD is satisfying_(IP) & not I_KD is satisfying_(OP) )
by ka, n1, K1; verum