theorem Th16: :: BAGORD_2:29

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