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;
A3:
the ToleranceRel of (pcs-reverse P) = the ToleranceRel of P `
by Def40;
let p, p9, q, q9 be Element of (pcs-reverse P); PCS_0:def 22 ( p (--) q & p9 <= p & q9 <= q implies p9 (--) q9 )
assume that
A4:
[p,q] in the ToleranceRel of (pcs-reverse P)
and
A5:
[p9,p] in the InternalRel of (pcs-reverse P)
and
A6:
[q9,q] in the InternalRel of (pcs-reverse P)
; ORDERS_2:def 5,PCS_0:def 7 p9 (--) q9
A7:
p9 in the carrier of (pcs-reverse P)
by A5, ZFMISC_1:87;
reconsider p90 = p9, q90 = q9, p0 = p, q0 = q as Element of P by Def40;
not [p0,q0] in the ToleranceRel of P
by A3, A4, XBOOLE_0:def 5;
then A8:
not p0 (--) q0
;
A9:
[p0,p90] in the InternalRel of P
by A2, A5, RELAT_1:def 7;
A10:
[q0,q90] in the InternalRel of P
by A2, A6, RELAT_1:def 7;
A11:
p0 <= p90
by A9;
q0 <= q90
by A10;
then
not p90 (--) q90
by A8, A11, Def22;
then A12:
not [p90,q90] in the ToleranceRel of P
;
[p9,q9] in [: the carrier of P, the carrier of P:]
by A1, A7, ZFMISC_1:87;
hence
[p9,q9] in the ToleranceRel of (pcs-reverse P)
by A3, A12, XBOOLE_0:def 5; PCS_0:def 7 verum