theorem
for
A,
B,
C being
Point of
(TOP-REAL 2) for
a,
b,
r being
Real st
A,
B,
C is_a_triangle &
angle (
C,
B,
A)
in ].0,PI.[ &
angle (
B,
A,
C)
in ].0,PI.[ &
A in circle (
a,
b,
r) &
B in circle (
a,
b,
r) &
C in circle (
a,
b,
r) &
|[a,b]| in LSeg (
A,
C) holds
angle (
C,
B,
A)
= PI / 2