E-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:50;
then A1: E-max (L~ (Cage C,n)) in rng (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by FINSEQ_6:96, SPRECT_2:47;
len (Upper_Seq C,n) = (E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by Th12;
hence not Upper_Seq C,n is empty by A1, FINSEQ_4:31; :: thesis: verum