theorem
Th29
:
:: EUCLID12:37
for
A
,
B
,
C
being
Point
of
(
TOPREAL
2
)
for
r
being
Real
st
A
<>
B
&
r
is
positive
&
r
<>
1 &
.
(
A

C
)
.
=
r
*
.
(
A

B
)
.
holds
A
,
B
,
C
are_mutually_distinct