for n being Element of NAT
for T being connected admissible TermOrder of n
for P being non empty Subset of (Bags n) ex b being bag of n st
( b in P & ( for b9 being bag of n st b9 in P holds
b <= b9,T ) )