let n be Nat; :: thesis: for R being Subset of REAL
for p1, p2, q1 being Point of () st R = { |.(q1 - p).| where p is Point of () : p in Line (p1,p2) } holds
ex q2 being Point of () 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 () st R = { |.(q1 - p).| where p is Point of () : p in Line (p1,p2) } holds
ex q2 being Point of () st
( q2 in Line (p1,p2) & |.(q1 - q2).| = lower_bound R & p1 - p2,q1 - q2 are_orthogonal )

let p1, p2, q1 be Point of (); :: thesis: ( R = { |.(q1 - p).| where p is Point of () : p in Line (p1,p2) } implies ex q2 being Point of () 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 () by EUCLID:22;
assume A7: R = { |.(q1 - p).| where p is Point of () : p in Line (p1,p2) } ; :: thesis: ex q2 being Point of () 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
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 ; :: thesis: verum
end;
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
proof
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 () such that
A12: ( r = |.(q1 - p0).| & p0 in Line (p1,p2) ) by A7;
the carrier of () = the carrier of () by EUCLID:67;
then reconsider x = p0 as Element of REAL n ;
thus |.(q1 - q2).| <= r by A2, A6, A12; :: thesis: verum
end;
R is bounded_below
proof
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 () such that
A13: ( r = |.(q1 - p0).| & p0 in Line (p1,p2) ) by A7;
the carrier of () = the carrier of () by EUCLID:67;
then reconsider x = p0 as Element of REAL n ;
thus |.(q1 - q2).| <= r by A2, A6, A13; :: thesis: verum
end;
then ( y1 - y2 = q1 - q2 & |.(q1 - q2).| = lower_bound R ) by ;
hence ex q2 being Point of () st
( q2 in Line (p1,p2) & |.(q1 - q2).| = lower_bound R & p1 - p2,q1 - q2 are_orthogonal ) by A2, A4, A5, A3; :: thesis: verum