defpred S1[ set ] means $1 is TolSet of T;
let Z1, Z2 be set ; ( ( for Y being set holds
( Y in Z1 iff Y is TolSet of T ) ) & ( for Y being set holds
( Y in Z2 iff Y is TolSet of T ) ) implies Z1 = Z2 )
assume that
A3:
for Y being set holds
( Y in Z1 iff S1[Y] )
and
A4:
for Y being set holds
( Y in Z2 iff S1[Y] )
; Z1 = Z2
Z1 = Z2
from XFAMILY:sch 2(A3, A4);
hence
Z1 = Z2
; verum