let x, y be Element of [.0,1.]; ( x > y implies (1 - x) + y >= y / x )
assume S0:
x > y
; (1 - x) + y >= y / x
1 - x in [.0,1.]
by FUZNORM1:7;
then
1 - x >= 0
by XXREAL_1:1;
then
(1 - x) * x >= (1 - x) * y
by S0, XREAL_1:64;
then a1:
((1 - x) * x) + (x * y) >= ((1 - x) * y) + (x * y)
by XREAL_1:6;
S2:
x > 0
by S0, XXREAL_1:1;
then
(x * ((1 - x) + y)) / x >= y / x
by a1, XREAL_1:72;
hence
(1 - x) + y >= y / x
by XCMPLX_1:89, S2; verum