let n be 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 )
let R be 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 )
let p1, p2, q1 be Point of (TOP-REAL n); ( R = { |.(q1 - p).| where p is Point of (TOP-REAL n) : p in Line (p1,p2) } implies 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 ) )
reconsider y1 = q1 as Element of REAL n by EUCLID:22;
consider x1, x2 being Element of REAL n such that
A1:
( p1 = x1 & p2 = x2 )
and
A2:
Line (x1,x2) = Line (p1,p2)
by Lm8;
A3:
x1 - x2 = p1 - p2
by A1;
consider y2 being Element of REAL n such that
A4:
y2 in Line (x1,x2)
and
A5:
x1 - x2,y1 - y2 are_orthogonal
and
A6:
for x being Element of REAL n st x in Line (x1,x2) holds
|.(y1 - y2).| <= |.(y1 - x).|
by Lm7;
reconsider q2 = y2 as Point of (TOP-REAL n) by EUCLID:22;
assume A7:
R = { |.(q1 - p).| where p is Point of (TOP-REAL n) : p in Line (p1,p2) }
; 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 )
A8:
for s being Real st 0 < s holds
ex r being Real st
( r in R & r < |.(q1 - q2).| + s )
p1 in Line (p1,p2)
by RLTOPSP1:72;
then A10:
|.(q1 - p1).| in R
by A7;
A11:
for r being Real st r in R holds
|.(q1 - q2).| <= r
R is bounded_below
then
( y1 - y2 = q1 - q2 & |.(q1 - q2).| = lower_bound R )
by A10, A8, A11, SEQ_4:def 2;
hence
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 )
by A2, A4, A5, A3; verum