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