defpred S₁[ set ] means $1 is TolClass of T;
let C1, C2 be set ; :: thesis: ( ( for Y being set holds
( Y in C1 iff Y is TolClass of T ) ) & ( for Y being set holds
( Y in C2 iff Y is TolClass of T ) ) implies C1 = C2 )
assume that
A7: for Y being set holds
( Y in C1 iff S₁[Y] ) and
A8: for Y being set holds
( Y in C2 iff S₁[Y] ) ; :: thesis: C1 = C2
C1 = C2 from XFAMILY:sch 2(A7, A8);
hence C1 = C2 ; :: thesis: verum