theorem Th7: :: JORDAN1C:7
for C being compact Subset of (TOP-REAL 2) st BDD C <> {} holds
E-bound C >= E-bound (BDD C)