:: deftheorem defines PartialOrdered OPOSET_1:def 14 :
for O being non empty OrthoRelStr holds
( O is PartialOrdered iff ( O is reflexive & O is antisymmetric & O is transitive ) );