for n being Nat
for A being Subset of (TOP-REAL n) st A is being_line holds
ex p1, p2 being Point of (TOP-REAL n) st
( p1 in A & p2 in A & p1 <> p2 )