let n be Ordinal; :: thesis: for T being TermOrder of n
for b being bag of n holds b in field T
let T be TermOrder of n; :: thesis: for b being bag of n holds b in field T
let b be bag of n; :: thesis: b in field T
field T = Bags n by ORDERS_1:12;
then A1: T is_reflexive_in Bags n by RELAT_2:def 9;
b is Element of Bags n by PRE_POLY:def 12;
then [b,b] in T by A1, RELAT_2:def 1;
hence b in field T by RELAT_1:15; :: thesis: verum