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