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)

set g = I_LK ;

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

proof

hence
I_FD <= I_LK
by FUZNORM1:def 16; :: thesis: verum
let x, y be Element of [.0,1.]; :: thesis: I_FD . (x,y) <= I_LK . (x,y)

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

end;

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

then
I_LK . (x,y) = 1
by Lemma01;

hence I_FD . (x,y) <= I_LK . (x,y) by A0, FUZIMPL1:def 23; :: thesis: verum

end;hence I_FD . (x,y) <= I_LK . (x,y) by A0, FUZIMPL1:def 23; :: thesis: verum

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

then A3:
I_FD . (x,y) = max ((1 - x),y)
by FUZIMPL1:def 23;

A4: I_LK . (x,y) = (1 - x) + y by A2, Lemma01;

0 <= y by XXREAL_1:1;

then A5: (1 - x) + 0 <= (1 - x) + y by XREAL_1:6;

1 - x in [.0,1.] by FUZNORM1:7;

then 0 <= 1 - x by XXREAL_1:1;

then 0 + y <= (1 - x) + y by XREAL_1:6;

hence I_FD . (x,y) <= I_LK . (x,y) by A3, XXREAL_0:28, A4, A5; :: thesis: verum

end;A4: I_LK . (x,y) = (1 - x) + y by A2, Lemma01;

0 <= y by XXREAL_1:1;

then A5: (1 - x) + 0 <= (1 - x) + y by XREAL_1:6;

1 - x in [.0,1.] by FUZNORM1:7;

then 0 <= 1 - x by XXREAL_1:1;

then 0 + y <= (1 - x) + y by XREAL_1:6;

hence I_FD . (x,y) <= I_LK . (x,y) by A3, XXREAL_0:28, A4, A5; :: thesis: verum