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

proof

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

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

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

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

end;

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

then I_FD . (x,y) = max ((1 - x),y) by FUZIMPL1:def 23;
hence I_KD . (x,y) <= I_FD . (x,y) by FUZIMPL1:def 18; :: thesis: verum

end;

end;

end;

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