theorem Th8: :: JCT_MISC:8

for A, B being Subset of REAL
for C, D being non empty Subset of REAL st C c= A & D c= B holds
dist (A,B) <= dist (C,D)