defpred S1[ set ] means $1 is TolClass of T;
consider Z being set such that
A5: for x being set holds
( x in Z iff ( x in bool X & S1[x] ) ) from XFAMILY:sch 1();
 take Z ; :: thesis: for Y being set holds
( Y in Z iff Y is TolClass of T )
let Y be set ; :: thesis: ( Y in Z iff Y is TolClass of T )
thus ( Y in Z implies Y is TolClass of T ) by A5; :: thesis: ( Y is TolClass of T implies Y in Z )
assume A6: Y is TolClass 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 A6, Def1;
hence x in X by ZFMISC_1:87; :: thesis: verum
end;
then Y c= X ;
hence Y in Z by A5, A6; :: thesis: verum