Upper_Seq C,n is_sequence_on Gauge C,n by Th4;
hence Upper_Seq C,n is standard by JORDAN8:7; :: thesis: verum