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

proof

let y be Element of [.0,1.]; :: thesis: I_KD . (1,y) = y
T1: 0 <= y by XXREAL_1:1;
I_KD . (1,y) = max ((1 - 1),y) by K1, FUZIMPL1:def 18
.= y by T1, XXREAL_0:def 10 ;
hence I_KD . (1,y) = y ; :: thesis: verum

end;

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.]; :: thesis: 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; :: thesis: 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; :: thesis: verum