defpred S₁[ Nat] means $1 is prime ;
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 prime )
let n be Nat; :: thesis: ( n in X iff n is prime )
thus ( n in X implies n is prime ) by A1; :: thesis: ( n is prime implies n in X )
assume A2: n is prime ; :: thesis: n in X
n in NAT by ORDINAL1:def 12;
hence n in X by A1, A2; :: thesis: verum