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)
A1: Lower_Seq C,n = (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) -: (W-min (L~ (Cage C,n))) by Th26;
W-min (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:47;
then A2: 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;
(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)))) ;
then W-min (L~ (Cage C,n)) in rng (Lower_Seq C,n) by A1, A2, FINSEQ_5:49;
then A3: 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 A3, REVROT_1:1; :: thesis: verum