set f = I_KD ;
set g = I_RC ;
for x, y being Element of [.0,1.] holds I_KD . (x,y) <= I_RC . (x,y)
proof
let x,
y be
Element of
[.0,1.];
I_KD . (x,y) <= I_RC . (x,y)
x * y in [.0,1.]
by FUZNORM1:3;
then
x * y >= 0
by XXREAL_1:1;
then A1:
(1 - x) + 0 <= (1 - x) + (x * y)
by XREAL_1:6;
(x * y) + ((1 - x) * 1) in [.y,1.]
by Lemma00;
then
y <= (1 - x) + (x * y)
by XXREAL_1:1;
then
max (
(1 - x),
y)
<= (1 - x) + (x * y)
by A1, XXREAL_0:28;
then
I_KD . (
x,
y)
<= (1 - x) + (x * y)
by FUZIMPL1:def 18;
hence
I_KD . (
x,
y)
<= I_RC . (
x,
y)
by FUZIMPL1:def 17;
verum
end;
hence
I_KD <= I_RC
by FUZNORM1:def 16; verum