defpred S₁[ set ] means $1 is TolSet of T;
let Z1, Z2 be set ; :: thesis: ( ( 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 S₁[Y] ) and
A4: for Y being set holds
( Y in Z2 iff S₁[Y] ) ; :: thesis: Z1 = Z2
Z1 = Z2 from XFAMILY:sch 2(A3, A4);
hence Z1 = Z2 ; :: thesis: verum