set I = I_RS ;

A1: I_RS is satisfying_(OP) by FUZIMPL1:def 20;

K1: ( 1 in [.0,1.] & 1 / 2 in [.0,1.] & 0 in [.0,1.] ) by XXREAL_1:1;

then I_RS . (1,(1 / 2)) <> 1 / 2 by FUZIMPL1:def 20;

then not I_RS is satisfying_(NP) by K1;

hence ( not I_RS is satisfying_(NP) & not I_RS is satisfying_(EP) & I_RS is satisfying_(IP) & I_RS is satisfying_(OP) ) by A1; :: thesis: verum

A1: I_RS is satisfying_(OP) by FUZIMPL1:def 20;

K1: ( 1 in [.0,1.] & 1 / 2 in [.0,1.] & 0 in [.0,1.] ) by XXREAL_1:1;

then I_RS . (1,(1 / 2)) <> 1 / 2 by FUZIMPL1:def 20;

then not I_RS is satisfying_(NP) by K1;

hence ( not I_RS is satisfying_(NP) & not I_RS is satisfying_(EP) & I_RS is satisfying_(IP) & I_RS is satisfying_(OP) ) by A1; :: thesis: verum