let n be Ordinal; :: thesis: for T being admissible TermOrder of n
for b being bag of n holds EmptyBag n <= b,T
let T be admissible TermOrder of n; :: thesis: for b being bag of n holds EmptyBag n <= b,T
let b be bag of n; :: thesis: EmptyBag n <= b,T
[(EmptyBag n),b] in T by BAGORDER:def 5;
hence EmptyBag n <= b,T by Def2; :: thesis: verum