for n being Nat
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st n is_sufficiently_large_for C holds
n >= 1