let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n being Element of NAT holds (Upper_Seq C,n) /. (len (Upper_Seq C,n)) = E-max (L~ (Cage C,n))
let n be Element of NAT ; :: thesis: (Upper_Seq C,n) /. (len (Upper_Seq C,n)) = E-max (L~ (Cage C,n))
A1: ( Upper_Seq C,n = (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) -: (E-max (L~ (Cage C,n))) & rng (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) = rng (Cage C,n) ) by FINSEQ_6:96, JORDAN1E:def 1, SPRECT_2:47;
then 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, SPRECT_2:50;
hence (Upper_Seq C,n) /. (len (Upper_Seq C,n)) = E-max (L~ (Cage C,n)) by A1, FINSEQ_5:48, SPRECT_2:50; :: thesis: verum