theorem
Th36
:
:: EUCLID12:48
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
L1
__
L2
&
L1
=
Line
(
A
,
B
) &
L2
=
Line
(
C
,
D
) holds
(
(
B

A
)
,
(
D

C
)
)
=
0