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

C
)
.
=
(
1
/
2
)
*
.
(
A

B
)
.
holds
.
(
B

C
)
.
=
(
1
/
2
)
*
.
(
A

B
)
.