:: deftheorem defines StrictPartialOrdered OPOSET_1:def 16 :
for O being non empty OrthoRelStr holds
( O is StrictPartialOrdered iff ( O is asymmetric & O is transitive ) );