for R being non empty transitive asymmetric RelStr
for a, b being Element of (DershowitzMannaOrder R) st a <= b holds
b <> EmptyBag the carrier of R