theorem Th10: :: JCT_MISC:10

for A, B being non empty compact Subset of REAL holds dist (A,B) >= 0