len (Lower_Seq (C,n)) >= 3 by Th19;
then len (Lower_Seq (C,n)) >= 2 by XXREAL_0:2;
hence Lower_Seq (C,n) is being_S-Seq by TOPREAL1:def 8; :: thesis: verum