theorem Th40: :: BAGORD_2:54

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 = b | { x where x is Element of R : x is_maximal_in support b }