let n be Element of NAT ; :: thesis: for z1, x being Element of COMPLEX n
for A being Subset of (COMPLEX n) st A <> {} holds
|.(z1 - x).| + (dist (x,A)) >= dist (z1,A)
let z1, x be Element of COMPLEX n; :: thesis: for A being Subset of (COMPLEX n) st A <> {} holds
|.(z1 - x).| + (dist (x,A)) >= dist (z1,A)
let A be Subset of (COMPLEX n); :: thesis: ( A <> {} implies |.(z1 - x).| + (dist (x,A)) >= dist (z1,A) )
x + (z1 - x) = z1 by Th50;
hence ( A <> {} implies |.(z1 - x).| + (dist (x,A)) >= dist (z1,A) ) by Th86; :: thesis: verum