R partially_orders X by ORDERS_1:44;
hence R |_2 A is Order of A by ORDERS_1:35, ORDERS_1:45; :: thesis: verum