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)

set g = I_WB ;

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

proof

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

end;A1: ( x <= 1 & y <= 1 ) by XXREAL_1:1;

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

end;

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;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

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;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