set R = pcs-reverse P;
A1: the carrier of (pcs-reverse P) = the carrier of P by Def40;
A2: the InternalRel of (pcs-reverse P) = the InternalRel of P ~ by Def40;
the InternalRel of P is_transitive_in the carrier of P by ORDERS_2:def 3;
hence the InternalRel of (pcs-reverse P) is_transitive_in the carrier of (pcs-reverse P) by A1, A2, ORDERS_1:80; :: according to ORDERS_2:def 3 :: thesis: verum