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)

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

end;

suppose
x > y
; :: thesis: I_RC . (x,y) <= I_LK . (x,y)

then C2:
I_LK . (x,y) = (1 - x) + y
by Lemma01;

C3: I_RC . (x,y) = (1 - x) + (x * y) by FUZIMPL1:def 17;

( y >= 0 & x <= 1 ) by XXREAL_1:1;

then x * y <= 1 * y by XREAL_1:64;

hence I_RC . (x,y) <= I_LK . (x,y) by C2, C3, XREAL_1:6; :: thesis: verum

end;C3: I_RC . (x,y) = (1 - x) + (x * y) by FUZIMPL1:def 17;

( y >= 0 & x <= 1 ) by XXREAL_1:1;

then x * y <= 1 * y by XREAL_1:64;

hence I_RC . (x,y) <= I_LK . (x,y) by C2, C3, XREAL_1:6; :: thesis: verum