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 )
proof
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;
x1 in Line (x1,x2) by Th9;
then A7: |.(y1 - x1).| in R by A4;
A8: for r being Real st r in R holds
|.(y1 - y2).| <= r
proof
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;
R is bounded_below
proof
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;
then |.(y1 - y2).| = lower_bound R by A7, A5, A8, SEQ_4:def 2;
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