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

proof

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;

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

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