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; verum