let A be Order; :: thesis: the InternalRel of A partially_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 & the InternalRel of A is_antisymmetric_in the carrier of A ) by ORDERS_2:def 2, ORDERS_2:def 3, ORDERS_2:def 4;
hence the InternalRel of A partially_orders the carrier of A by ORDERS_1:def 8; :: thesis: verum