set P = pcs-total D;
thus ( pcs-total D is reflexive & pcs-total D is transitive ) ; :: according to PCS_0:def 23 :: thesis: ( pcs-total D is pcs-tol-reflexive & pcs-total D is pcs-tol-symmetric & pcs-total D is pcs-compatible )
thus ( pcs-total D is pcs-tol-reflexive & pcs-total D is pcs-tol-symmetric ) ; :: thesis: pcs-total D is pcs-compatible
let p, p9, q, q9 be Element of (pcs-total D); :: according to PCS_0:def 22 :: thesis: ( p (--) q & p9 <= p & q9 <= q implies p9 (--) q9 )
assume p (--) q ; :: thesis: ( not p9 <= p or not q9 <= q or p9 (--) q9 )
assume that
A1: p9 <= p and
q9 <= q ; :: thesis: p9 (--) q9
[p9,p] in [:D,D:] by A1;
then p9 in the carrier of (pcs-total D) by ZFMISC_1:87;
hence [p9,q9] in the ToleranceRel of (pcs-total D) by ZFMISC_1:87; :: according to PCS_0:def 7 :: thesis: verum