theorem :: EUCLID_4:47

for n being Nat
for R being Subset of REAL
for p1, p2, q1 being Point of (TOP-REAL n) st R = { |.(q1 - p).| where p is Point of (TOP-REAL n) : p in Line (p1,p2) } holds
ex q2 being Point of (TOP-REAL n) st
( q2 in Line (p1,p2) & |.(q1 - q2).| = lower_bound R & p1 - p2,q1 - q2 are_orthogonal )