let X be ManySortedSet of I; :: thesis: ( X = pcs-ToleranceRels C iff for i being Element of I holds X . i = the ToleranceRel of (C . i) )
thus ( X = pcs-ToleranceRels C implies for i being Element of I holds X . i = the ToleranceRel of (C . i) ) :: thesis: ( ( for i being Element of I holds X . i = the ToleranceRel of (C . i) ) implies X = pcs-ToleranceRels C )

proof

assume A1: X = pcs-ToleranceRels C ; :: thesis: for i being Element of I holds X . i = the ToleranceRel of (C . i)
let i be Element of I; :: thesis: X . i = the ToleranceRel of (C . i)
ex P being TolStr st
( P = C . i & X . i = the ToleranceRel of P ) by A1, Def19;
hence X . i = the ToleranceRel of (C . i) ; :: thesis: verum

end;

assume A2: for i being Element of I holds X . i = the ToleranceRel of (C . i) ; :: thesis: X = pcs-ToleranceRels C
for i being set st i in I holds
ex P being TolStr st
( P = C . i & X . i = the ToleranceRel of P )

proof

let i be set ; :: thesis: ( i in I implies ex P being TolStr st
( P = C . i & X . i = the ToleranceRel of P ) )
assume i in I ; :: thesis: ex P being TolStr st
( P = C . i & X . i = the ToleranceRel of P )
then reconsider i = i as Element of I ;
take C . i ; :: thesis: ( C . i = C . i & X . i = the ToleranceRel of (C . i) )
thus ( C . i = C . i & X . i = the ToleranceRel of (C . i) ) by A2; :: thesis: verum

end;

hence X = pcs-ToleranceRels C by Def19; :: thesis: verum