:: deftheorem Def12 defines QuasiOrdered OPOSET_1:def 12 :
for O being non empty RelStr holds
( O is QuasiOrdered iff ( O is reflexive & O is transitive ) );