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)

set g = I_RC ;

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

proof

hence
I_KD <= I_RC
by FUZNORM1:def 16; :: thesis: verum
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;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