for n being Nat
for x, x1, x2 being Element of REAL n
for L being Element of line_of_REAL n st L = Line (x1,x2) holds
{ |.(x - x0).| where x0 is Element of REAL n : x0 in Line (x1,x2) } = dist_v (x,L) ;