theorem Th15: :: TERMORD:15

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