let O be non empty OrthoRelStr ; :: thesis: ( O is SubPartialOrdered iff O is PartialOrdered )
thus ( O is SubPartialOrdered implies O is PartialOrdered ) :: thesis: ( O is PartialOrdered implies O is SubPartialOrdered )

proof

assume O is SubPartialOrdered ; :: thesis: O is PartialOrdered
then reconsider O = O as non empty reflexive SubAntisymmetric SubTransitive OrthoRelStr by Def24;
( O is SubAntisymmetric & O is SubTransitive ) ;
hence O is PartialOrdered by Def25; :: thesis: verum

end;

assume O is PartialOrdered ; :: thesis: O is SubPartialOrdered
then reconsider O = O as non empty reflexive transitive antisymmetric OrthoRelStr by Def25;
O is SubTransitive ;
hence O is SubPartialOrdered by Def24; :: thesis: verum