defpred S₁[ set ] means ex n being Nat st
( n = $1 & n is square-free & ( for i being Prime st i divides n holds
i <= p ) );
ex X being Subset of NAT st
for x being Element of NAT holds
( x in X iff S₁[x] ) from SUBSET_1:sch 3();
then consider X being Subset of NAT such that
A1: for x being Element of NAT holds
( x in X iff S₁[x] ) ;
take X ; :: thesis: for n being Nat holds
( n in X iff ( n is square-free & ( for i being Prime st i divides n holds
i <= p ) ) )
let n be Nat; :: thesis: ( n in X iff ( n is square-free & ( for i being Prime st i divides n holds
i <= p ) ) )

hereby :: thesis: ( n is square-free & ( for i being Prime st i divides n holds
i <= p ) implies n in X )

assume n in X ; :: thesis: ( n is square-free & ( for i being Prime st i divides n holds
i <= p ) )
then consider m being Nat such that
B1: ( m = n & m is square-free & ( for i being Prime st i divides m holds
i <= p ) ) by A1;
thus ( n is square-free & ( for i being Prime st i divides n holds
i <= p ) ) by B1; :: thesis: verum

end;

assume b2: ( n is square-free & ( for i being Prime st i divides n holds
i <= p ) ) ; :: thesis: n in X
n in NAT by ORDINAL1:def 12;
hence n in X by A1, b2; :: thesis: verum