theorem Th57: :: EUCLIDLP:57

for n being Nat
for x being Element of REAL n
for L being Element of line_of_REAL n ex x0 being Element of REAL n st
( x0 in L & |.(x - x0).| = dist (x,L) )