theorem Th9: :: JORDAN1F:9

for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds
( ( L~ (Upper_Seq (C,n)) = Upper_Arc (L~ (Cage (C,n))) & L~ (Lower_Seq (C,n)) = Lower_Arc (L~ (Cage (C,n))) ) or ( L~ (Upper_Seq (C,n)) = Lower_Arc (L~ (Cage (C,n))) & L~ (Lower_Seq (C,n)) = Upper_Arc (L~ (Cage (C,n))) ) )