theorem :: TOPREAL1:8

for n being Nat
for p, p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) holds
(LSeg (p1,p)) /\ (LSeg (p,p2)) = {p}