theorem
Th27
:
:: EUCLID12:34
for
A
,
B
,
C
being
Point
of
(
TOPREAL
2
)
st
C
in
LSeg
(
A
,
B
) &
.
(
A

C
)
.
=
.
(
B

C
)
.
holds
half_length
(
A
,
B
)
=
.
(
A

C
)
.