theorem
:: EUCLID12:23
for
A
,
B
being
Point
of
(
TOP-REAL
2
)
holds
half_length
(
A
,
B
)
=
half_length
(
B
,
A
)
by
EUCLID_6:43
;