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, p', q, q' be Element of ; :: according to PCS_0:def 22 :: thesis: ( p (--) q & p' <= p & q' <= q implies p' (--) q' )
assume p (--) q ; :: thesis: ( not p' <= p or not q' <= q or p' (--) q' )
assume that
A1: p' <= p and
q' <= q ; :: thesis: p' (--) q'
[p',p] in [:D,D:] by A1, ORDERS_2:def 9;
then p' in the carrier of (pcs-total D) by ZFMISC_1:106;
hence [p',q'] in the ToleranceRel of (pcs-total D) by ZFMISC_1:106; :: according to PCS_0:def 7 :: thesis: verum