let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: 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))) ) )
let n be Nat; :: thesis: ( ( 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))) ) )
set WC = W-min (L~ (Cage (C,n)));
set EC = E-max (L~ (Cage (C,n)));
A1: ( Lower_Arc (L~ (Cage (C,n))) is_an_arc_of W-min (L~ (Cage (C,n))), E-max (L~ (Cage (C,n))) & (Upper_Arc (L~ (Cage (C,n)))) \/ (Lower_Arc (L~ (Cage (C,n)))) = L~ (Cage (C,n)) ) by JORDAN6:50;
( (Upper_Seq (C,n)) /. 1 = W-min (L~ (Cage (C,n))) & (Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) = E-max (L~ (Cage (C,n))) ) by Th5, Th7;
then A2: L~ (Upper_Seq (C,n)) is_an_arc_of W-min (L~ (Cage (C,n))), E-max (L~ (Cage (C,n))) by TOPREAL1:25;
( (Lower_Seq (C,n)) /. 1 = E-max (L~ (Cage (C,n))) & (Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) = W-min (L~ (Cage (C,n))) ) by Th6, Th8;
then A3: L~ (Lower_Seq (C,n)) is_an_arc_of W-min (L~ (Cage (C,n))), E-max (L~ (Cage (C,n))) by JORDAN5B:14, TOPREAL1:25;
( (L~ (Upper_Seq (C,n))) \/ (L~ (Lower_Seq (C,n))) = L~ (Cage (C,n)) & Upper_Arc (L~ (Cage (C,n))) is_an_arc_of W-min (L~ (Cage (C,n))), E-max (L~ (Cage (C,n))) ) by JORDAN1E:13, JORDAN6:50;
hence ( ( 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))) ) ) by A2, A3, A1, JORDAN6:48; :: thesis: verum