let A be Preorder; :: thesis: the InternalRel of A quasi_orders the carrier of A
( the InternalRel of A is_reflexive_in the carrier of A & the InternalRel of A is_transitive_in the carrier of A ) by ORDERS_2:def 2, ORDERS_2:def 3;
hence the InternalRel of A quasi_orders the carrier of A by ORDERS_1:def 7; :: thesis: verum