set P = pcs-union C;
set TR = the ToleranceRel of (pcs-union C);
set CP = the carrier of (pcs-union C);
A1: the ToleranceRel of (pcs-union C) = Union (pcs-ToleranceRels C) by Def36;
let x, y be object ; :: according to RELAT_2:def 3,PCS_0:def 11 :: thesis: ( not x in the carrier of (pcs-union C) or not y in the carrier of (pcs-union C) or not [^,^] in the ToleranceRel of (pcs-union C) or [^,^] in the ToleranceRel of (pcs-union C) )
assume that
x in the carrier of (pcs-union C) and
y in the carrier of (pcs-union C) ; :: thesis: ( not [^,^] in the ToleranceRel of (pcs-union C) or [^,^] in the ToleranceRel of (pcs-union C) )
assume [x,y] in the ToleranceRel of (pcs-union C) ; :: thesis: [^,^] in the ToleranceRel of (pcs-union C)
then consider P being set such that
A2: [x,y] in P and
A3: P in rng (pcs-ToleranceRels C) by A1, TARSKI:def 4;
consider i being object such that
A4: i in dom (pcs-ToleranceRels C) and
A5: (pcs-ToleranceRels C) . i = P by A3, FUNCT_1:def 3;
reconsider I = I as non empty set by A4;
reconsider C = C as pcs-tol-symmetric-yielding () ManySortedSet of I ;
reconsider i = i as Element of I by A4;
A6: (pcs-ToleranceRels C) . i = the ToleranceRel of (C . i) by Def20;
then A7: x in the carrier of (C . i) by A2, A5, ZFMISC_1:87;
A8: y in the carrier of (C . i) by A2, A5, A6, ZFMISC_1:87;
the ToleranceRel of (C . i) is_symmetric_in the carrier of (C . i) by Def11;
then A9: [y,x] in the ToleranceRel of (C . i) by A2, A5, A6, A7, A8;
the ToleranceRel of (C . i) in rng (pcs-ToleranceRels C) by A4, A6, FUNCT_1:3;
hence [^,^] in the ToleranceRel of (pcs-union C) by A1, A9, TARSKI:def 4; :: thesis: verum