let n be Nat; :: thesis: for x being Element of REAL n
for L being Element of line_of_REAL n holds dist (x,L) >= 0
let x be Element of REAL n; :: thesis: for L being Element of line_of_REAL n holds dist (x,L) >= 0
let L be Element of line_of_REAL n; :: thesis: dist (x,L) >= 0
ex x0 being Element of REAL n st
( x0 in L & |.(x - x0).| = dist (x,L) ) by Th57;
hence dist (x,L) >= 0 ; :: thesis: verum