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_reflexive_in the carrier of P by ORDERS_2:def 2;
hence the InternalRel of (pcs-reverse P) is_reflexive_in the carrier of (pcs-reverse P) by A1, A2, ORDERS_1:79; :: according to ORDERS_2:def 2 :: thesis: verum