R partially_orders X by ORDERS_1:140;
hence R |_2 A is Order of A by ORDERS_1:131, ORDERS_1:141; :: thesis: verum