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