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