let
x
,
y
be
R_eal
;
:: thesis:
y

x
<=
.
(
x

y
)
.

.
(
x

y
)
.
<=
x

y
by
EXTREAL1:20
;
then

(
x

y
)
<=
.
(
x

y
)
.
by
XXREAL_3:60
;
hence
y

x
<=
.
(
x

y
)
.
by
XXREAL_3:26
;
:: thesis:
verum