theorem :: BAGORD_2:39

for R being non empty transitive asymmetric RelStr
for a being bag of the carrier of R holds
( <*a*> is ordered iff ( a <> EmptyBag the carrier of R & ( for x, y being Element of R st a . x > 0 & a . y > 0 & x <> y holds
x ## y ) ) )