theorem
Th38
:
:: EUCLID12:50
for
A
,
B
,
C
being
Point
of
(
TOP-REAL
2
)
for
L1
,
L2
being
Element
of
line_of_REAL
2 st
L1
_|_
L2
&
C
in
L1
/\
L2
&
A
in
L1
&
B
in
L2
&
A
<>
C
&
B
<>
C
& not
angle
(
A
,
C
,
B
)
=
PI
/
2 holds
angle
(
A
,
C
,
B
)
=
(
3
*
PI
)
/
2