:: deftheorem defines dist_v EUCLIDLP:def 5 :
for n being Nat
for x being Element of REAL n
for L being Element of line_of_REAL n holds dist_v (x,L) = { |.(x - x0).| where x0 is Element of REAL n : x0 in L } ;