let QO be non empty QuasiOrdered OrthoRelStr ; :: thesis: ( QO is antisymmetric implies QO is PartialOrdered )
assume A1: QO is antisymmetric ; :: thesis: QO is PartialOrdered
( QO is reflexive & QO is transitive ) by Def22;
hence QO is PartialOrdered by A1; :: thesis: verum