for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds
( rng (Upper_Seq (C,n)) c= rng (Cage (C,n)) & rng (Lower_Seq (C,n)) c= rng (Cage (C,n)) )