defpred S₁[ natural number ] means not $1 is square-containing ;
consider X being Subset of NAT such that
A1: for n being Element of NAT holds
( n in X iff S₁[n] ) from SUBSET_1:sch 3();
take X ; :: thesis: for n being natural number holds
( n in X iff not n is square-containing )
let n be natural number ; :: thesis: ( n in X iff not n is square-containing )
thus ( n in X implies not n is square-containing ) by A1; :: thesis: ( not n is square-containing implies n in X )
assume A2: not n is square-containing ; :: thesis: n in X
n is Element of NAT by INT_1:16;
hence n in X by A1, A2; :: thesis: verum