theorem Th32A: :: BAGORD_2:49

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