theorem
Th39
:
:: EUCLID12:52
for
A
,
B
,
C
being
Point
of
(
TOPREAL
2
)
for
L1
being
Element
of
line_of_REAL
2 st
A
<>
B
&
L1
=
Line
(
A
,
B
) &
C
in
LSeg
(
A
,
B
) &
.
(
A

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

B
)
.
holds
ex
L2
being
Element
of
line_of_REAL
2 st
(
C
in
L2
&
L1
__
L2
)