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

let R be Subset of REAL; :: thesis: 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 )

let x1, x2, y1 be Element of REAL n; :: thesis: ( R = { |.(y1 - x).| where x is Element of REAL n : x in Line (x1,x2) } implies ex y2 being Element of REAL n st

( y2 in Line (x1,x2) & |.(y1 - y2).| = lower_bound R & x1 - x2,y1 - y2 are_orthogonal ) )

consider y2 being Element of REAL n such that

A1: y2 in Line (x1,x2) and

A2: x1 - x2,y1 - y2 are_orthogonal and

A3: for x being Element of REAL n st x in Line (x1,x2) holds

|.(y1 - y2).| <= |.(y1 - x).| by Lm7;

assume A4: R = { |.(y1 - x).| where x is Element of REAL n : x in Line (x1,x2) } ; :: thesis: ex y2 being Element of REAL n st

( y2 in Line (x1,x2) & |.(y1 - y2).| = lower_bound R & x1 - x2,y1 - y2 are_orthogonal )

A5: for s being Real st 0 < s holds

ex r being Real st

( r in R & r < |.(y1 - y2).| + s )

then A7: |.(y1 - x1).| in R by A4;

A8: for r being Real st r in R holds

|.(y1 - y2).| <= r

hence ex y2 being Element of REAL n st

( y2 in Line (x1,x2) & |.(y1 - y2).| = lower_bound R & x1 - x2,y1 - y2 are_orthogonal ) by A1, A2; :: thesis: verum

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 )

let R be Subset of REAL; :: thesis: 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 )

let x1, x2, y1 be Element of REAL n; :: thesis: ( R = { |.(y1 - x).| where x is Element of REAL n : x in Line (x1,x2) } implies ex y2 being Element of REAL n st

( y2 in Line (x1,x2) & |.(y1 - y2).| = lower_bound R & x1 - x2,y1 - y2 are_orthogonal ) )

consider y2 being Element of REAL n such that

A1: y2 in Line (x1,x2) and

A2: x1 - x2,y1 - y2 are_orthogonal and

A3: for x being Element of REAL n st x in Line (x1,x2) holds

|.(y1 - y2).| <= |.(y1 - x).| by Lm7;

assume A4: R = { |.(y1 - x).| where x is Element of REAL n : x in Line (x1,x2) } ; :: thesis: ex y2 being Element of REAL n st

( y2 in Line (x1,x2) & |.(y1 - y2).| = lower_bound R & x1 - x2,y1 - y2 are_orthogonal )

A5: for s being Real st 0 < s holds

ex r being Real st

( r in R & r < |.(y1 - y2).| + s )

proof

x1 in Line (x1,x2)
by Th9;
let s be Real; :: thesis: ( 0 < s implies ex r being Real st

( r in R & r < |.(y1 - y2).| + s ) )

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

( r in R & r < |.(y1 - y2).| + s )

take |.(y1 - y2).| ; :: thesis: ( |.(y1 - y2).| in R & |.(y1 - y2).| < |.(y1 - y2).| + s )

thus ( |.(y1 - y2).| in R & |.(y1 - y2).| < |.(y1 - y2).| + s ) by A4, A1, A6, XREAL_1:29; :: thesis: verum

end;( r in R & r < |.(y1 - y2).| + s ) )

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

( r in R & r < |.(y1 - y2).| + s )

take |.(y1 - y2).| ; :: thesis: ( |.(y1 - y2).| in R & |.(y1 - y2).| < |.(y1 - y2).| + s )

thus ( |.(y1 - y2).| in R & |.(y1 - y2).| < |.(y1 - y2).| + s ) by A4, A1, A6, XREAL_1:29; :: thesis: verum

then A7: |.(y1 - x1).| in R by A4;

A8: for r being Real st r in R holds

|.(y1 - y2).| <= r

proof

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

assume r in R ; :: thesis: |.(y1 - y2).| <= r

then ex x0 being Element of REAL n st

( r = |.(y1 - x0).| & x0 in Line (x1,x2) ) by A4;

hence |.(y1 - y2).| <= r by A3; :: thesis: verum

end;assume r in R ; :: thesis: |.(y1 - y2).| <= r

then ex x0 being Element of REAL n st

( r = |.(y1 - x0).| & x0 in Line (x1,x2) ) by A4;

hence |.(y1 - y2).| <= r by A3; :: thesis: verum

proof

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

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

assume r in R ; :: thesis: |.(y1 - y2).| <= r

then ex x0 being Element of REAL n st

( r = |.(y1 - x0).| & x0 in Line (x1,x2) ) by A4;

hence |.(y1 - y2).| <= r by A3; :: thesis: verum

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

assume r in R ; :: thesis: |.(y1 - y2).| <= r

then ex x0 being Element of REAL n st

( r = |.(y1 - x0).| & x0 in Line (x1,x2) ) by A4;

hence |.(y1 - y2).| <= r by A3; :: thesis: verum

hence ex y2 being Element of REAL n st

( y2 in Line (x1,x2) & |.(y1 - y2).| = lower_bound R & x1 - x2,y1 - y2 are_orthogonal ) by A1, A2; :: thesis: verum