theorem Th9: :: JCT_MISC:9

for A, B being non empty compact Subset of REAL ex r, s being Real st
( r in A & s in B & dist (A,B) = |.(r - s).| )