theorem :: BAGORD_2:31

for R1, R2 being non empty transitive asymmetric RelStr st the carrier of R1 = the carrier of R2 & the InternalRel of R1 c= the InternalRel of R2 holds
the InternalRel of (DershowitzMannaOrder R1) c= the InternalRel of (DershowitzMannaOrder R2)