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