defpred S₁[ set ] means $1 is TolSet of T;
consider Z being set such that
A1: for x being set holds
( x in Z iff ( x in bool X & S₁[x] ) ) from XFAMILY:sch 1();
take Z ; :: thesis: for Y being set holds
( Y in Z iff Y is TolSet of T )
let Y be set ; :: thesis: ( Y in Z iff Y is TolSet of T )
thus ( Y in Z implies Y is TolSet of T ) by A1; :: thesis: ( Y is TolSet of T implies Y in Z )
assume A2: Y is TolSet of T ; :: thesis: Y in Z
for x being object st x in Y holds
x in X

proof

let x be object ; :: thesis: ( x in Y implies x in X )
assume x in Y ; :: thesis: x in X
then [x,x] in T by A2, Def1;
hence x in X by ZFMISC_1:87; :: thesis: verum

end;

then Y c= X ;
hence Y in Z by A1, A2; :: thesis: verum