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

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

proof

for x, y, z being Element of [.0,1.] holds I_RC . (x,(I_RC . (y,z))) = I_RC . (y,(I_RC . (x,z)))
let y be Element of [.0,1.]; :: thesis: I_RC . (1,y) = y

1 in [.0,1.] by XXREAL_1:1;

then I_RC . (1,y) = (1 - 1) + (1 * y) by FUZIMPL1:def 17

.= y ;

hence I_RC . (1,y) = y ; :: thesis: verum

end;1 in [.0,1.] by XXREAL_1:1;

then I_RC . (1,y) = (1 - 1) + (1 * y) by FUZIMPL1:def 17

.= y ;

hence I_RC . (1,y) = y ; :: thesis: verum

proof

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; :: thesis: verum
let x, y, z be Element of [.0,1.]; :: thesis: 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; :: thesis: verum

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