theorem Th2: :: POLYNOM6:2

for n being Ordinal
for a, b being bag of n st a < b holds
ex o being Ordinal st
( o in n & a . o < b . o & ( for l being Ordinal st l in o holds
a . l = b . l ) )