let n be Element of 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 Th62;
hence dist x,L >= 0 ; :: thesis: verum