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