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