let T be admissible TermOrder of n; :: thesis: T is well_founded
T is well-ordering by BAGORDER:34;
hence T is well_founded by WELLORD1:def 4; :: thesis: verum