let n be Element of NAT ; :: thesis: for x being Element of REAL n
for L being Element of line_of_REAL n ex x0 being Element of REAL n st
( x0 in L & |.(x - x0).| = dist x,L )
let x be Element of REAL n; :: thesis: for L being Element of line_of_REAL n ex x0 being Element of REAL n st
( x0 in L & |.(x - x0).| = dist x,L )
let L be Element of line_of_REAL n; :: thesis: ex x0 being Element of REAL n st
( x0 in L & |.(x - x0).| = dist x,L )
consider x1, x2 being Element of REAL n such that
A1: L = Line x1,x2 by Th56;
{ |.(x - x').| where x' is Element of REAL n : x' in Line x1,x2 } = dist_v x,L by A1;
then reconsider R = { |.(x - x').| where x' is Element of REAL n : x' in Line x1,x2 } as Subset of REAL ;
consider x0 being Element of REAL n such that
A2: ( x0 in Line x1,x2 & |.(x - x0).| = lower_bound R & x1 - x2,x - x0 are_orthogonal ) by EUCLID_4:45;
take x0 ; :: thesis: ( x0 in L & |.(x - x0).| = dist x,L )
thus ( x0 in L & |.(x - x0).| = dist x,L ) by A1, A2; :: thesis: verum