theorem :: JORDAN1E:13

for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds L~ (Cage (C,n)) = (L~ (Upper_Seq (C,n))) \/ (L~ (Lower_Seq (C,n)))