theorem Th6: :: TOPREAL1:6
for n being Nat
for p1, p2, q1, q2 being Point of (TOP-REAL n) st q1 in LSeg (p1,p2) & q2 in LSeg (p1,p2) holds
LSeg (q1,q2) c= LSeg (p1,p2)