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

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

B
)
.
&
C
in
L2
&
L1
__
L2
&
D
in
L2
holds
.
(
D

A
)
.
=
.
(
D

B
)
.