set f = I_RS ;
set g = I_GD ;
for x, y being Element of [.0,1.] holds I_RS . (x,y) <= I_GD . (x,y)

proof

let x, y be Element of [.0,1.]; :: thesis: I_RS . (x,y) <= I_GD . (x,y)

per cases ( x <= y or x > y ) ;

suppose x <= y ; :: thesis: I_RS . (x,y) <= I_GD . (x,y)

then I_GD . (x,y) = 1 by FUZIMPL1:def 16;
hence I_RS . (x,y) <= I_GD . (x,y) by XXREAL_1:1; :: thesis: verum

end;

suppose x > y ; :: thesis: I_RS . (x,y) <= I_GD . (x,y)

then I_RS . (x,y) = 0 by FUZIMPL1:def 20;
hence I_RS . (x,y) <= I_GD . (x,y) by XXREAL_1:1; :: thesis: verum

end;

end;

end;

hence I_RS <= I_GD by FUZNORM1:def 16; :: thesis: verum