let n be Element of NAT ; :: thesis: for A, B being Subset of (COMPLEX n) st A meets B holds
dist A,B = 0
let A, B be Subset of (COMPLEX n); :: thesis: ( A meets B implies dist A,B = 0 )
assume A meets B ; :: thesis: dist A,B = 0
then consider z being set such that
A1: z in A and
A2: z in B by XBOOLE_0:3;
reconsider z = z as Element of COMPLEX n by A1;
( dist z,A = 0 & dist z,B = 0 ) by A1, A2, Th87;
then 0 + 0 >= dist A,B by A1, A2, Th100;
hence dist A,B = 0 by A1, A2, Th98; :: thesis: verum