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

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

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

n1: I_KD . ((1 / 2),(1 / 2)) =
max ((1 - (1 / 2)),(1 / 2))
by FUZIMPL1:def 18, K1
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;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

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

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