theorem :: JORDAN1E:17
for n being Nat
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds Upper_Seq (C,n) is_in_the_area_of Cage (C,n)