theorem :: EUCLID_4:43

for n being Nat
for p1, p2, q1, q2 being Point of (TOP-REAL n) st q1 in Line (p1,p2) & q2 in Line (p1,p2) & q1 <> q2 holds
Line (p1,p2) c= Line (q1,q2) by RLTOPSP1:75;