let O be non empty RelStr ; :: thesis: ( O is QuasiOrdered implies O is SubQuasiOrdered )
assume A1: O is QuasiOrdered ; :: thesis: O is SubQuasiOrdered
set IntRel = the InternalRel of O;
set CO = the carrier of O;
A2: ( O is reflexive & O is transitive ) by A1, Def22;
then the InternalRel of O is_reflexive_in the carrier of O by ORDERS_2:def 4;
then A3: ( the InternalRel of O is reflexive & field the InternalRel of O = the carrier of O ) by Th7;
the InternalRel of O is_transitive_in the carrier of O by A2, ORDERS_2:def 5;
then A4: the InternalRel of O is transitive by Th13;
A5: O is SubReFlexive by A3, Def9;
O is SubTransitive by A4, Def19;
hence O is SubQuasiOrdered by A5, Def21; :: thesis: verum