theorem :: BAGORD_2:59

for R being non empty transitive asymmetric RelStr
for b being bag of the carrier of R holds
( b = EmptyBag the carrier of R iff OrderedPartition b = {} )