theorem Th34: :: BAGORD_2:53

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 holds
( x is_maximal_in support b iff a . x > 0 )