theorem Th10: :: JORDAN1E:10

for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds (len (Upper_Seq (C,n))) + (len (Lower_Seq (C,n))) = (len (Cage (C,n))) + 1