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.];
I_FD . (x,y) <= I_LK . (x,y)
per cases
( x <= y or x > y )
;
suppose A2:
x > y
;
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;
verum end; end;
end;
hence
I_FD <= I_LK
by FUZNORM1:def 16; verum