defpred S₁[ set , set ] means ex R being TolStr st
( R = C . $1 & $2 = the ToleranceRel of R );
A1: for i being set st i in I holds
ex j being set st S₁[i,j]

proof

let i be set ; :: thesis: ( i in I implies ex j being set st S₁[i,j] )
assume A2: i in I ; :: thesis: ex j being set st S₁[i,j]
then reconsider I = I as non empty set ;
reconsider B = C as () ManySortedSet of ;
reconsider i' = i as Element of I by A2;
take j = the ToleranceRel of (B . i'); :: thesis: S₁[i,j]
take R = B . i'; :: thesis: ( R = C . i & j = the ToleranceRel of R )
thus ( R = C . i & j = the ToleranceRel of R ) ; :: thesis: verum

end;

consider M being Function such that
A3: dom M = I and
A4: for i being set st i in I holds
S₁[i,M . i] from CLASSES1:sch 1(A1);
M is ManySortedSet of by A3, PARTFUN1:def 4, RELAT_1:def 18;
hence ex b₁ being ManySortedSet of st
for i being set st i in I holds
ex P being TolStr st
( P = C . i & b₁ . i = the ToleranceRel of P ) by A4; :: thesis: verum