theorem
for
p,
p1,
q being
Point of
(TOP-REAL 2) for
r being
Real for
u being
Point of
(Euclid 2) st not
p1 in Ball (
u,
r) &
p in Ball (
u,
r) &
|[(q `1),(p `2)]| in Ball (
u,
r) & not
|[(q `1),(p `2)]| in LSeg (
p1,
p) &
p1 `2 = p `2 &
p `1 <> q `1 &
p `2 <> q `2 holds
((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}