theorem
Th18
:
:: EUCLID12:25
for
A
,
B
being
Point
of
(
TOPREAL
2
)
holds
.
(
A

(
(
1
/
2
)
*
(
A
+
B
)
)
)
.
=
(
1
/
2
)
*
.
(
A

B
)
.