let n be Nat; :: thesis: 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; :: thesis: 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); :: thesis: ( 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) } ; :: thesis: 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 )

then A10: |.(q1 - p1).| in R by A7;

A11: for r being Real st r in R holds

|.(q1 - q2).| <= r

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; :: thesis: verum

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; :: thesis: 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); :: thesis: ( 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) } ; :: thesis: 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 )

proof

p1 in Line (p1,p2)
by RLTOPSP1:72;
let s be Real; :: thesis: ( 0 < s implies ex r being Real st

( r in R & r < |.(q1 - q2).| + s ) )

assume A9: 0 < s ; :: thesis: ex r being Real st

( r in R & r < |.(q1 - q2).| + s )

take |.(q1 - q2).| ; :: thesis: ( |.(q1 - q2).| in R & |.(q1 - q2).| < |.(q1 - q2).| + s )

thus ( |.(q1 - q2).| in R & |.(q1 - q2).| < |.(q1 - q2).| + s ) by A7, A2, A4, A9, XREAL_1:29; :: thesis: verum

end;( r in R & r < |.(q1 - q2).| + s ) )

assume A9: 0 < s ; :: thesis: ex r being Real st

( r in R & r < |.(q1 - q2).| + s )

take |.(q1 - q2).| ; :: thesis: ( |.(q1 - q2).| in R & |.(q1 - q2).| < |.(q1 - q2).| + s )

thus ( |.(q1 - q2).| in R & |.(q1 - q2).| < |.(q1 - q2).| + s ) by A7, A2, A4, A9, XREAL_1:29; :: thesis: verum

then A10: |.(q1 - p1).| in R by A7;

A11: for r being Real st r in R holds

|.(q1 - q2).| <= r

proof

R is bounded_below
let r be Real; :: thesis: ( r in R implies |.(q1 - q2).| <= r )

assume r in R ; :: thesis: |.(q1 - q2).| <= r

then consider p0 being Point of (TOP-REAL n) such that

A12: ( r = |.(q1 - p0).| & p0 in Line (p1,p2) ) by A7;

the carrier of (Euclid n) = the carrier of (TOP-REAL n) by EUCLID:67;

then reconsider x = p0 as Element of REAL n ;

thus |.(q1 - q2).| <= r by A2, A6, A12; :: thesis: verum

end;assume r in R ; :: thesis: |.(q1 - q2).| <= r

then consider p0 being Point of (TOP-REAL n) such that

A12: ( r = |.(q1 - p0).| & p0 in Line (p1,p2) ) by A7;

the carrier of (Euclid n) = the carrier of (TOP-REAL n) by EUCLID:67;

then reconsider x = p0 as Element of REAL n ;

thus |.(q1 - q2).| <= r by A2, A6, A12; :: thesis: verum

proof

then
( y1 - y2 = q1 - q2 & |.(q1 - q2).| = lower_bound R )
by A10, A8, A11, SEQ_4:def 2;
take
|.(q1 - q2).|
; :: according to XXREAL_2:def 9 :: thesis: |.(q1 - q2).| is LowerBound of R

let r be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not r in R or |.(q1 - q2).| <= r )

assume r in R ; :: thesis: |.(q1 - q2).| <= r

then consider p0 being Point of (TOP-REAL n) such that

A13: ( r = |.(q1 - p0).| & p0 in Line (p1,p2) ) by A7;

the carrier of (Euclid n) = the carrier of (TOP-REAL n) by EUCLID:67;

then reconsider x = p0 as Element of REAL n ;

thus |.(q1 - q2).| <= r by A2, A6, A13; :: thesis: verum

end;let r be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not r in R or |.(q1 - q2).| <= r )

assume r in R ; :: thesis: |.(q1 - q2).| <= r

then consider p0 being Point of (TOP-REAL n) such that

A13: ( r = |.(q1 - p0).| & p0 in Line (p1,p2) ) by A7;

the carrier of (Euclid n) = the carrier of (TOP-REAL n) by EUCLID:67;

then reconsider x = p0 as Element of REAL n ;

thus |.(q1 - q2).| <= r by A2, A6, A13; :: thesis: verum

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; :: thesis: verum