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

proof

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

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

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

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

end;

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

then C2: I_GD . (x,y) = y by FUZIMPL1:def 16;
C3: I_GG . (x,y) = y / x by FUZIMPL1:def 19, C1;
y >= 0 by XXREAL_1:1;
hence I_GD . (x,y) <= I_GG . (x,y) by C2, C3, Lemma11, C1; :: thesis: verum

end;

end;

end;

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