theorem Th5: :: TOPREAL1:5

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