for R being non empty transitive asymmetric RelStr holds DivOrder the carrier of R c= the InternalRel of (DershowitzMannaOrder R)