let n be Nat; :: thesis: for x, z1 being Element of COMPLEX n
for A being Subset of (COMPLEX n) st A <> {} holds
|.(z1 - x).| + (dist (x,A)) >= dist (z1,A)
let x, z1 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 Th79;
hence ( A <> {} implies |.(z1 - x).| + (dist (x,A)) >= dist (z1,A) ) by Th114; :: thesis: verum