let n be Nat; :: thesis: for z1, z2 being Element of COMPLEX n st z1 <> z2 holds
0 < |.(z1 - z2).|
let z1, z2 be Element of COMPLEX n; :: thesis: ( z1 <> z2 implies 0 < |.(z1 - z2).| )
assume z1 <> z2 ; :: thesis: 0 < |.(z1 - z2).|
then 0 <> |.(z1 - z2).| by Th101;
hence 0 < |.(z1 - z2).| by Th94; :: thesis: verum