theorem :: OPOSET_1:10

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