theorem :: EUCLID_4:14

for n being Nat
for x1 being Element of REAL n
for A being Subset of (REAL n) st A is being_line holds
ex x2 being Element of REAL n st
( x1 <> x2 & x2 in A )