for n being Nat
for p1, p2 being Point of (TOP-REAL n)
for g being Path of p1,p2 st rng g c= LSeg (p1,p2) holds
rng g = LSeg (p1,p2)