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
consider x0 being Element of REAL n such that
A1: ( x0 in L & |.(x - x0).| = dist x,L ) by Th62;
thus dist x,L >= 0 by A1; :: thesis: verum