theorem Th6: :: SPRECT_3:6

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