let X1, X2 be Subset of NAT; :: thesis: ( ( for n being Nat holds
( n in X1 iff n is square-free ) ) & ( for n being Nat holds
( n in X2 iff n is square-free ) ) implies X1 = X2 )
defpred S₁[ Nat] means $1 is square-free ;
assume that
A3: for n being Nat holds
( n in X1 iff n is square-free ) and
A4: for n being Nat holds
( n in X2 iff n is square-free ) ; :: thesis: X1 = X2
A5: for y being Element of NAT holds
( y in X2 iff S₁[y] ) by A4;
A6: for y being Element of NAT holds
( y in X1 iff S₁[y] ) by A3;
thus X1 = X2 from SUBSET_1:sch 2(A6, A5); :: thesis: verum