:: deftheorem defines dist EUCLIDLP:def 6 :
for n being Nat
for x being Element of REAL n
for L being Element of line_of_REAL n holds dist (x,L) = lower_bound (dist_v (x,L));