set f = I_LK ;
set g = I_WB ;
for x, y being Element of [.0,1.] holds I_LK . (x,y) <= I_WB . (x,y)
proof
let x, y be Element of [.0,1.]; :: thesis: I_LK . (x,y) <= I_WB . (x,y)
A1: ( x <= 1 & y <= 1 ) by XXREAL_1:1;
per cases ( x = 1 or x <> 1 ) ;
suppose A2: x = 1 ; :: thesis: I_LK . (x,y) <= I_WB . (x,y)
then B1: I_WB . (x,y) = y by FUZIMPL1:def 22;
min (1,((1 - x) + y)) = y by A1, A2, XXREAL_0:def 9;
hence I_LK . (x,y) <= I_WB . (x,y) by B1, FUZIMPL1:def 14; :: thesis: verum
end;
suppose x <> 1 ; :: thesis: I_LK . (x,y) <= I_WB . (x,y)
then x < 1 by A1, XXREAL_0:1;
then I_WB . (x,y) = 1 by FUZIMPL1:def 22;
hence I_LK . (x,y) <= I_WB . (x,y) by XXREAL_1:1; :: thesis: verum
end;
end;
end;
hence I_LK <= I_WB by FUZNORM1:def 16; :: thesis: verum