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

(
the_midpoint_of_the_segment
(
A
,
B
)
)
)
.
=
.
(
(
the_midpoint_of_the_segment
(
A
,
B
)
)

B
)
.