defpred S₁[ Element of ] means $1 is_associated_to a;
let X1, X2 be Subset of ; :: thesis: ( ( for b being Element of holds
( b in X1 iff b is_associated_to a ) ) & ( for b being Element of holds
( b in X2 iff b is_associated_to a ) ) implies X1 = X2 )
assume that
A2: for y being Element of holds
( y in X1 iff S₁[y] ) and
A3: for y being Element of holds
( y in X2 iff S₁[y] ) ; :: thesis: X1 = X2
thus X1 = X2 from SUBSET_1:sch 2(A2, A3); :: thesis: verum