for n being Nat
for p1, p2 being Point of (TOP-REAL n) holds
( p1 in Line (p1,p2) & p2 in Line (p1,p2) ) by RLTOPSP1:72;