E-max (L~ (Cage (C,n))) in rng (Cage (C,n))
by SPRECT_2:46;

then A2: 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 (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 Th9;

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:21;

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:19;

hence not Lower_Seq (C,n) is empty by XREAL_1:10; :: thesis: verum

then A2: 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 (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 Th9;

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:21;

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:19;

hence not Lower_Seq (C,n) is empty by XREAL_1:10; :: thesis: verum