let T be admissible TermOrder of n; :: thesis: T is well_founded
n in NAT by ORDINAL1:def 13;
then T is well-ordering by BAGORDER:35;
hence T is well_founded by WELLORD1:def 4; :: thesis: verum