let I be set ; :: thesis: for C being () ManySortedSet of I
for p, q being Element of (pcs-union C) holds
( p (--) q iff ex i being object ex P being pcs-Str ex p9, q9 being Element of P st
( i in I & P = C . i & p9 = p & q9 = q & p9 (--) q9 ) )
let C be () ManySortedSet of I; :: thesis: for p, q being Element of (pcs-union C) holds
( p (--) q iff ex i being object ex P being pcs-Str ex p9, q9 being Element of P st
( i in I & P = C . i & p9 = p & q9 = q & p9 (--) q9 ) )
set R = pcs-union C;
let p, q be Element of (pcs-union C); :: thesis: ( p (--) q iff ex i being object ex P being pcs-Str ex p9, q9 being Element of P st
( i in I & P = C . i & p9 = p & q9 = q & p9 (--) q9 ) )
A1: dom (pcs-ToleranceRels C) = I by PARTFUN1:def 2;
thus ( p (--) q implies ex i being object ex P being pcs-Str ex p9, q9 being Element of P st
( i in I & P = C . i & p9 = p & q9 = q & p9 (--) q9 ) ) :: thesis: ( ex i being object ex P being pcs-Str ex p9, q9 being Element of P st
( i in I & P = C . i & p9 = p & q9 = q & p9 (--) q9 ) implies p (--) q )

proof

assume p (--) q ; :: thesis: ex i being object ex P being pcs-Str ex p9, q9 being Element of P st
( i in I & P = C . i & p9 = p & q9 = q & p9 (--) q9 )
then [p,q] in the ToleranceRel of (pcs-union C) ;
then [p,q] in Union (pcs-ToleranceRels C) by Def36;
then consider Z being set such that
A2: [p,q] in Z and
A3: Z in rng (pcs-ToleranceRels C) by TARSKI:def 4;
consider i being object such that
A4: i in dom (pcs-ToleranceRels C) and
A5: (pcs-ToleranceRels C) . i = Z by A3, FUNCT_1:def 3;
reconsider I1 = I as non empty set by A4;
reconsider A1 = C as () ManySortedSet of I1 ;
reconsider i1 = i as Element of I1 by A4;
reconsider P = A1 . i1 as pcs-Str ;
take i ; :: thesis: ex P being pcs-Str ex p9, q9 being Element of P st
( i in I & P = C . i & p9 = p & q9 = q & p9 (--) q9 )
take P ; :: thesis: ex p9, q9 being Element of P st
( i in I & P = C . i & p9 = p & q9 = q & p9 (--) q9 )
Z = the ToleranceRel of (A1 . i1) by A5, Def20;
then reconsider p9 = p, q9 = q as Element of P by A2, ZFMISC_1:87;
take p9 ; :: thesis: ex q9 being Element of P st
( i in I & P = C . i & p9 = p & q9 = q & p9 (--) q9 )
take q9 ; :: thesis: ( i in I & P = C . i & p9 = p & q9 = q & p9 (--) q9 )
thus i in I by A4; :: thesis: ( P = C . i & p9 = p & q9 = q & p9 (--) q9 )
thus ( P = C . i & p9 = p & q9 = q ) ; :: thesis: p9 (--) q9
thus [p9,q9] in the ToleranceRel of P by A2, A5, Def20; :: according to PCS_0:def 7 :: thesis: verum

end;

given i being object , P being pcs-Str , p9, q9 being Element of P such that A6: i in I and
A7: P = C . i and
A8: p9 = p and
A9: q9 = q and
A10: p9 (--) q9 ; :: thesis: p (--) q
A11: [p9,q9] in the ToleranceRel of P by A10;
reconsider I1 = I as non empty set by A6;
reconsider i1 = i as Element of I1 by A6;
reconsider A1 = C as () ManySortedSet of I1 ;
(pcs-ToleranceRels A1) . i1 = the ToleranceRel of (A1 . i1) by Def20;
then the ToleranceRel of (A1 . i1) in rng (pcs-ToleranceRels C) by A1, FUNCT_1:3;
then [p,q] in Union (pcs-ToleranceRels C) by A7, A8, A9, A11, TARSKI:def 4;
hence [p,q] in the ToleranceRel of (pcs-union C) by Def36; :: according to PCS_0:def 7 :: thesis: verum