:: deftheorem defines SubQuasiOrdered OPOSET_1:def 11 :
for O being non empty RelStr holds
( O is SubQuasiOrdered iff ( O is SubReFlexive & O is transitive ) );