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) &
|[(p `1),(q `2)]| in Ball (
u,
r) & not
|[(p `1),(q `2)]| in LSeg (
p1,
p) &
p1 `1 = p `1 &
p `1 <> q `1 &
p `2 <> q `2 holds
((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p}