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) /. 1 = W-min (L~ (Cage C,n))
let n be Element of NAT ; :: thesis: (Upper_Seq C,n) /. 1 = W-min (L~ (Cage C,n))
E-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:50;
then ( 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)) in rng (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) ) by FINSEQ_6:96, JORDAN1E:def 1, SPRECT_2:47;
then ( W-min (L~ (Cage C,n)) in rng (Cage C,n) & (Upper_Seq C,n) /. 1 = (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. 1 ) by FINSEQ_5:47, SPRECT_2:47;
hence (Upper_Seq C,n) /. 1 = W-min (L~ (Cage C,n)) by FINSEQ_6:98; :: thesis: verum