let
a
,
b
,
c
be
positive
Real
;
:: thesis:
(
a
<
b
implies 1
<
(
b
+
c
)
/
(
a
+
c
)
)
assume
a
<
b
;
:: thesis:
1
<
(
b
+
c
)
/
(
a
+
c
)
then
a
+
c
<
b
+
c
by
XREAL_1:8
;
hence
1
<
(
b
+
c
)
/
(
a
+
c
)
by
XREAL_1:187
;
:: thesis:
verum