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

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