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