theorem Th7: :: SPPOL_1:7

for n being Nat
for p1, p2, q1, q2 being Point of (TOP-REAL n) st LSeg (q1,q2) c= LSeg (p1,p2) & p1 in LSeg (q1,q2) & not p1 = q1 holds
p1 = q2