:: deftheorem OP defines OrderedPartition BAGORD_2:def 12 :
for R being non empty transitive asymmetric RelStr
for b being bag of the carrier of R
for b₃ being Bags the carrier of b₁ -valued FinSequence holds
( b₃ = OrderedPartition b iff ex F, G being Function of NAT,(Bags the carrier of R) st
( F . 0 = b & G . 0 = EmptyBag the carrier of R & ( for i being Nat holds
( G . (i + 1) = (F . i) | { x where x is Element of R : x is_maximal_in support (F . i) } & F . (i + 1) = (F . i) -' (G . (i + 1)) ) ) & ex i being Nat st
( F . i = EmptyBag the carrier of R & b₃ = G | (Seg i) & ( for j being Nat st j < i holds
F . j <> EmptyBag the carrier of R ) ) ) );