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)

set g = I_LK ;

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

proof

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