theorem Th12: :: OPOSET_1:12

for O being non empty OrthoRelStr st O is StrictPartialOrdered holds
O is irreflexive