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