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