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