let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n being Element of NAT st n > 0 holds
L~ (Upper_Seq C,n) = Upper_Arc (L~ (Cage C,n))
let n be Element of NAT ; :: thesis: ( n > 0 implies L~ (Upper_Seq C,n) = Upper_Arc (L~ (Cage C,n)) )
A1: W-min (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:47;
E-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:50;
then A2: E-max (L~ (Cage C,n)) in rng (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by FINSEQ_6:96, SPRECT_2:47;
A3: Upper_Seq C,n = (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) -: (E-max (L~ (Cage C,n))) by JORDAN1E:def 1;
then (Upper_Seq C,n) /. 1 = (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. 1 by A2, FINSEQ_5:47;
then A4: (Upper_Seq C,n) /. 1 = W-min (L~ (Cage C,n)) by A1, FINSEQ_6:98;
(Upper_Seq C,n) /. (len (Upper_Seq C,n)) = ((Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) -: (E-max (L~ (Cage C,n)))) /. ((E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))) by A3, A2, FINSEQ_5:45
.= E-max (L~ (Cage C,n)) by A2, FINSEQ_5:48 ;
then A5: L~ (Upper_Seq C,n) is_an_arc_of W-min (L~ (Cage C,n)), E-max (L~ (Cage C,n)) by A4, TOPREAL1:31;
assume n > 0 ; :: thesis: L~ (Upper_Seq C,n) = Upper_Arc (L~ (Cage C,n))
then A6: (First_Point (L~ (Upper_Seq C,n)),(W-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n))),(Vertical_Line (((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2))) `2 > (Last_Point (L~ (Lower_Seq C,n)),(E-max (L~ (Cage C,n))),(W-min (L~ (Cage C,n))),(Vertical_Line (((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2))) `2 by Th62;
A7: (Lower_Seq C,n) /. 1 = ((Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) :- (E-max (L~ (Cage C,n)))) /. 1 by JORDAN1E:def 2
.= E-max (L~ (Cage C,n)) by FINSEQ_5:56 ;
Lower_Seq C,n = (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) :- (E-max (L~ (Cage C,n))) by JORDAN1E:def 2;
then (Lower_Seq C,n) /. (len (Lower_Seq C,n)) = (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. (len (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))) by A2, FINSEQ_5:57
.= (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. 1 by FINSEQ_6:def 1
.= W-min (L~ (Cage C,n)) by A1, FINSEQ_6:98 ;
then A8: L~ (Lower_Seq C,n) is_an_arc_of E-max (L~ (Cage C,n)), W-min (L~ (Cage C,n)) by A7, TOPREAL1:31;
( (L~ (Upper_Seq C,n)) /\ (L~ (Lower_Seq C,n)) = {(W-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} & (L~ (Upper_Seq C,n)) \/ (L~ (Lower_Seq C,n)) = L~ (Cage C,n) ) by JORDAN1E:17, JORDAN1E:20;
hence L~ (Upper_Seq C,n) = Upper_Arc (L~ (Cage C,n)) by A5, A8, A6, JORDAN6:def 8; :: thesis: verum