for n being Nat
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds Rev (Lower_Seq (C,n)) is_a_h.c._for Cage (C,n)