let n be 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 object 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, Th115;
then 0 + 0 >= dist (A,B) by A1, A2, Th128;
hence dist (A,B) = 0 by A1, A2, Th126; :: thesis: verum