theorem Th126: :: SEQ_4:127

for n being Nat
for A, B being Subset of (COMPLEX n) st A <> {} & B <> {} holds
dist (A,B) >= 0