for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n, m being Nat st n <= m & n is_sufficiently_large_for C holds
m is_sufficiently_large_for C