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

proof

let x, y be Element of [.0,1.]; :: thesis: I_RC . (x,y) <= I_LK . (x,y)
(1 - x) + (x * y) in [.0,1.] by FUZIMPL1:3;
then A1: (1 - x) + (x * y) <= 1 by XXREAL_1:1;
A2: ( x >= 0 & y >= 0 ) by XXREAL_1:1;
x <= 1 by XXREAL_1:1;
then x * y <= 1 * y by A2, XREAL_1:64;
then (1 - x) + (x * y) <= (1 - x) + y by XREAL_1:6;
then (1 - x) + (x * y) <= min (1,((1 - x) + y)) by A1, XXREAL_0:20;
then I_RC . (x,y) <= min (1,((1 - x) + y)) by FUZIMPL1:def 17;
hence I_RC . (x,y) <= I_LK . (x,y) by FUZIMPL1:def 14; :: thesis: verum

end;

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