let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); 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; 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:50;
then
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;
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:45; verum