defpred S₁[ Nat] means $1 is square-free ;
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 Nat holds
( n in X iff n is square-free )
let n be Nat; :: thesis: ( n in X iff n is square-free )
thus ( n in X implies n is square-free ) by A1; :: thesis: ( n is square-free implies n in X )
assume A2: n is square-free ; :: thesis: n in X
n is Element of NAT by INT_1:3;
hence n in X by A1, A2; :: thesis: verum