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