theorem
Th22
:
:: EUCLID12:29
for
A
,
B
being
Point
of
(
TOP-REAL
2
)
holds
the_midpoint_of_the_segment
(
A
,
B
)
=
(
1
/
2
)
*
(
A
+
B
)