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

proof

let x, y be Element of [.0,1.]; :: thesis: I_KD . (x,y) <= I_RC . (x,y)
x * y in [.0,1.] by FUZNORM1:3;
then x * y >= 0 by XXREAL_1:1;
then A1: (1 - x) + 0 <= (1 - x) + (x * y) by XREAL_1:6;
(x * y) + ((1 - x) * 1) in [.y,1.] by Lemma00;
then y <= (1 - x) + (x * y) by XXREAL_1:1;
then max ((1 - x),y) <= (1 - x) + (x * y) by A1, XXREAL_0:28;
then I_KD . (x,y) <= (1 - x) + (x * y) by FUZIMPL1:def 18;
hence I_KD . (x,y) <= I_RC . (x,y) by FUZIMPL1:def 17; :: thesis: verum

end;

hence I_KD <= I_RC by FUZNORM1:def 16; :: thesis: verum