theorem :: ORDERS_5:29

for A being RelStr st the InternalRel of A quasi_orders the carrier of A holds
( A is reflexive & A is transitive ) by ORDERS_1:def 7, ORDERS_2:def 2, ORDERS_2:def 3;