let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n being Nat holds len (Upper_Seq (C,n)) = (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))

let n be Nat; :: thesis: len (Upper_Seq (C,n)) = (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))

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

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

hence len (Upper_Seq (C,n)) = (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_5:42; :: thesis: verum

let n be Nat; :: thesis: len (Upper_Seq (C,n)) = (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))

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

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

hence len (Upper_Seq (C,n)) = (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_5:42; :: thesis: verum