theorem :: OPOSET_1:9

for O being non empty RelStr st O is irreflexive & O is transitive holds
O is asymmetric ;