theorem Th31: :: BAGORD_2:47

for R being non empty transitive asymmetric RelStr
for a, b being bag of the carrier of R
for x being Element of R
for p being partition of b -' a
for q being partition of b st q is ordered & q = <*a*> ^ p & a . x > 0 holds
a . x = b . x