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 ) ) )
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