set P = pcs-union C;
set TR = the ToleranceRel of (pcs-union C);
set CP = the carrier of (pcs-union C);
set CA = Carrier C;
A1: the carrier of (pcs-union C) = Union (Carrier C) by Def36;
A2: the ToleranceRel of (pcs-union C) = Union (pcs-ToleranceRels C) by Def36;
A3: dom (pcs-ToleranceRels C) = I by PARTFUN1:def 2;
let x be object ; :: according to RELAT_2:def 1,PCS_0:def 9 :: thesis: ( not x in the carrier of (pcs-union C) or [^,^] in the ToleranceRel of (pcs-union C) )
assume x in the carrier of (pcs-union C) ; :: thesis: [^,^] in the ToleranceRel of (pcs-union C)
then consider P being set such that
A4: x in P and
A5: P in rng (Carrier C) by A1, TARSKI:def 4;
consider i being object such that
A6: i in dom (Carrier C) and
A7: (Carrier C) . i = P by A5, FUNCT_1:def 3;
A8: ex R being 1-sorted st
( R = C . i & (Carrier C) . i = the carrier of R ) by A6, PRALG_1:def 15;
reconsider I = I as non empty set by A6;
reconsider i = i as Element of I by A6;
reconsider C = C as pcs-tol-reflexive-yielding () ManySortedSet of I ;
A9: (pcs-ToleranceRels C) . i = the ToleranceRel of (C . i) by Def20;
the ToleranceRel of (C . i) is_reflexive_in the carrier of (C . i) by Def9;
then A10: [x,x] in the ToleranceRel of (C . i) by A4, A7, A8;
the ToleranceRel of (C . i) in rng (pcs-ToleranceRels C) by A3, A9, FUNCT_1:3;
hence [^,^] in the ToleranceRel of (pcs-union C) by A2, A10, TARSKI:def 4; :: thesis: verum