let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n being Nat st n > 0 holds

L~ (Upper_Seq (C,n)) = Upper_Arc (L~ (Cage (C,n)))

let n be 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:43;

E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;

then A2: E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:90, SPRECT_2:43;

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:44;

then A4: (Upper_Seq (C,n)) /. 1 = W-min (L~ (Cage (C,n))) by A1, FINSEQ_6:92;

(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:42

.= E-max (L~ (Cage (C,n))) by A2, FINSEQ_5:45 ;

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:25;

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 Th54;

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:53 ;

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:54

.= (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:92 ;

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:25;

( (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:13, JORDAN1E:16;

hence L~ (Upper_Seq (C,n)) = Upper_Arc (L~ (Cage (C,n))) by A5, A8, A6, JORDAN6:def 8; :: thesis: verum

L~ (Upper_Seq (C,n)) = Upper_Arc (L~ (Cage (C,n)))

let n be 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:43;

E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;

then A2: E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:90, SPRECT_2:43;

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:44;

then A4: (Upper_Seq (C,n)) /. 1 = W-min (L~ (Cage (C,n))) by A1, FINSEQ_6:92;

(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:42

.= E-max (L~ (Cage (C,n))) by A2, FINSEQ_5:45 ;

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:25;

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 Th54;

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:53 ;

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:54

.= (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:92 ;

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:25;

( (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:13, JORDAN1E:16;

hence L~ (Upper_Seq (C,n)) = Upper_Arc (L~ (Cage (C,n))) by A5, A8, A6, JORDAN6:def 8; :: thesis: verum