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) holds
Line (q1,q2) c= Line (p1,p2) by RLTOPSP1:74;