Lower_Seq C,n is_sequence_on Gauge C,n by Th5;
hence Lower_Seq C,n is standard by JORDAN8:7; :: thesis: verum