E-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:50;
then A2: 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 (Lower_Seq C,n) = ((len (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))) - ((E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))))) + 1 by Th13;
then ((len (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))) - (len (Lower_Seq C,n))) + 1 <= len (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by A2, FINSEQ_4:31;
then (len (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))) - (len (Lower_Seq C,n)) <= (len (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))) - 1 by XREAL_1:21;
hence not Lower_Seq C,n is empty by XREAL_1:12; :: thesis: verum