theorem :: TOPREAL3:42

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