for X1, X2 being Element of F₁() st ( for x being object holds
( x in X1 iff P₁[x] ) ) & ( for x being object holds
( x in X2 iff P₁[x] ) ) holds
X1 = X2