for n being Nat
for o being TermOrder of n st o is admissible holds
( the InternalRel of (NaivelyOrderedBags n) c= o & o is well-ordering )