let n be 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 Th51;
{ |.(x - x9).| where x9 is Element of REAL n : x9 in Line (x1,x2) } = dist_v (x,L) by A1;
then reconsider R = { |.(x - x9).| where x9 is Element of REAL n : x9 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 ) and
x1 - x2,x - x0 are_orthogonal by EUCLID_4:40;
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