theorem :: EUCLID_4:40

for n being Nat
for R being Subset of REAL
for x1, x2, y1 being Element of REAL n st R = { |.(y1 - x).| where x is Element of REAL n : x in Line (x1,x2) } holds
ex y2 being Element of REAL n st
( y2 in Line (x1,x2) & |.(y1 - y2).| = lower_bound R & x1 - x2,y1 - y2 are_orthogonal )