let n be Element of NAT ; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (W-min (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) = len (Lower_Seq (C,n))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: (W-min (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) = len (Lower_Seq (C,n))
W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:47;
then A1: W-min (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) by FINSEQ_6:96, SPRECT_2:50;
( Lower_Seq (C,n) = (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) -: (W-min (L~ (Cage (C,n)))) & (W-min (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) <= (W-min (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) ) by Th26;
then W-min (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) by A1, FINSEQ_5:49;
then A2: Lower_Seq (C,n) just_once_values W-min (L~ (Cage (C,n))) by FINSEQ_4:10;
(Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) = W-min (L~ (Cage (C,n))) by JORDAN1F:8;
hence (W-min (L~ (Cage (C,n)))) .. (Lower_Seq (C,n)) = len (Lower_Seq (C,n)) by A2, REVROT_1:1; :: thesis: verum