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