for X1, X2 being Subset of REAL st ( for x being R_eal holds
( x in X1 iff P₁[x] ) ) & ( for x being R_eal holds
( x in X2 iff P₁[x] ) ) holds
X1 = X2