let O be non empty RelStr ; :: thesis: ( O is QuasiOrdered implies O is SubQuasiOrdered )
set IntRel = the InternalRel of O;
set CO = the carrier of O;
assume A1: O is QuasiOrdered ; :: thesis: O is SubQuasiOrdered
then A2: O is transitive ;
O is reflexive by A1;
then the InternalRel of O is_reflexive_in the carrier of O ;
then the InternalRel of O is reflexive by PARTIT_2:21;
hence O is SubQuasiOrdered by A2, Def4; :: thesis: verum