defpred S₁[ set , set ] means ex X being set st
( X in C & $1 in X & $2 in X );
A1: for x being set st x in union C holds
S₁[x,x]

proof

let x be set ; :: thesis: ( x in union C implies S₁[x,x] )
assume A2: x in union C ; :: thesis: S₁[x,x]
take {x} ; :: thesis: ( {x} in C & x in {x} & x in {x} )
thus ( {x} in C & x in {x} & x in {x} ) by A2, Th4, TARSKI:def 1; :: thesis: verum

end;

A3: for x, y being set st x in union C & y in union C & S₁[x,y] holds
S₁[y,x] ;
consider T being Tolerance of (union C) such that
A4: for x, y being set st x in union C & y in union C holds
( [x,y] in T iff S₁[x,y] ) from TOLER_1:sch 1(A1, A3);
take T ; :: thesis: for x, y being object holds
( [x,y] in T iff ex X being set st
( X in C & x in X & y in X ) )
let x, y be object ; :: thesis: ( [x,y] in T iff ex X being set st
( X in C & x in X & y in X ) )
thus ( [x,y] in T implies ex X being set st
( X in C & x in X & y in X ) ) :: thesis: ( ex X being set st
( X in C & x in X & y in X ) implies [x,y] in T )

proof

assume A5: [x,y] in T ; :: thesis: ex X being set st
( X in C & x in X & y in X )
then ( x in union C & y in union C ) by ZFMISC_1:87;
hence ex X being set st
( X in C & x in X & y in X ) by A4, A5; :: thesis: verum

end;

given X being set such that A6: ( X in C & x in X & y in X ) ; :: thesis: [x,y] in T
( x in union C & y in union C ) by A6, TARSKI:def 4;
hence [x,y] in T by A4, A6; :: thesis: verum