theorem Th7: :: JCT_MISC:7

for A, B being Subset of REAL
for r, s being Real st r in A & s in B holds
|.(r - s).| >= dist (A,B)