set P = pcs-total D;
set IR = the InternalRel of (pcs-total D);
set TR = the ToleranceRel of (pcs-total D);
A1: field the InternalRel of (pcs-total D) = the carrier of (pcs-total D) by ORDERS_1:12;
hence the InternalRel of (pcs-total D) is_reflexive_in the carrier of (pcs-total D) by RELAT_2:def 9; :: according to ORDERS_2:def 2 :: thesis: ( pcs-total D is transitive & pcs-total D is pcs-tol-reflexive & pcs-total D is pcs-tol-symmetric )
thus the InternalRel of (pcs-total D) is_transitive_in the carrier of (pcs-total D) by A1, RELAT_2:def 16; :: according to ORDERS_2:def 3 :: thesis: ( pcs-total D is pcs-tol-reflexive & pcs-total D is pcs-tol-symmetric )
thus the ToleranceRel of (pcs-total D) is_reflexive_in the carrier of (pcs-total D) by A1, RELAT_2:def 9; :: according to PCS_0:def 9 :: thesis: pcs-total D is pcs-tol-symmetric
thus the ToleranceRel of (pcs-total D) is_symmetric_in the carrier of (pcs-total D) by A1, RELAT_2:def 11; :: according to PCS_0:def 11 :: thesis: verum