let C be compact non horizontal non vertical Subset of ; :: thesis: for n being Element of 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 Element of 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:65;
( (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:31;
( (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:31;
( (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:17, JORDAN6:65;
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:61; :: thesis: verum