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 O is transitive by Def22;
then the InternalRel of O is_transitive_in the carrier of O by ORDERS_2:def 5;
then the InternalRel of O is transitive by PARTIT_2:29;
then A2: O is transitive by Def19;
O is reflexive by A1, Def22;
then the InternalRel of O is_reflexive_in the carrier of O by ORDERS_2:def 4;
then the InternalRel of O is reflexive by PARTIT_2:23;
then O is SubReFlexive by Def9;
hence O is SubQuasiOrdered by A2, Def21; :: thesis: verum