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