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

proof

let x, y be Element of [.0,1.]; :: thesis: I_FD . (x,y) <= I_LK . (x,y)

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

suppose B1: x <= y ; :: thesis: I_FD . (x,y) <= I_LK . (x,y)

then I_FD . (x,y) = 1 by FUZIMPL1:def 23;
hence I_FD . (x,y) <= I_LK . (x,y) by B1, Lemma01; :: thesis: verum

end;

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

then C3: I_FD . (x,y) = max ((1 - x),y) by FUZIMPL1:def 23;
C2: I_LK . (x,y) = min (1,((1 - x) + y)) by FUZIMPL1:def 14;
max ((1 - x),y) in [.0,1.] by Lemma03;
then C1: max ((1 - x),y) <= 1 by XXREAL_1:1;
( y >= 0 & x >= 0 ) by XXREAL_1:1;
then D1: (1 - x) + 0 <= (1 - x) + y by XREAL_1:6;
1 - x in [.0,1.] by FUZNORM1:7;
then 1 - x >= 0 by XXREAL_1:1;
then 0 + y <= (1 - x) + y by XREAL_1:6;
then max ((1 - x),y) <= (1 - x) + y by D1, XXREAL_0:28;
hence I_FD . (x,y) <= I_LK . (x,y) by C1, C2, C3, XXREAL_0:20; :: thesis: verum

end;

end;

end;

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