theorem Th9: :: TOPREAL1:9

for n being Nat
for p1, p2 being Point of (TOP-REAL n) st p1 <> p2 holds
LSeg (p1,p2) is_an_arc_of p1,p2