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