theorem :: EUCLIDLP:59

for n being Nat
for x being Element of REAL n
for L being Element of line_of_REAL n holds
( x in L iff dist (x,L) = 0 )