theorem Th17: :: JORDAN2C:26

for n being Nat
for A being Subset of (TOP-REAL n) holds UBD A c= A `