theorem :: TOPREAL1:7

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