for n being Ordinal
for T being connected TermOrder of n
for b1, b2 being bag of n holds
( b1 <= max (b1,b2,T),T & b2 <= max (b1,b2,T),T )