E-max (L~ (Cage (C,n))) in rng (Cage (C,n))
by SPRECT_2:46;
then A1:
E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))
by FINSEQ_6:90, SPRECT_2:43;
len (Upper_Seq (C,n)) = (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))
by Th8;
hence
not Upper_Seq (C,n) is empty
by A1, FINSEQ_4:21; verum