theorem :: OPOSET_1:13

for QO being non empty QuasiOrdered OrthoRelStr st QO is antisymmetric holds
QO is PartialOrdered by Def12;