defpred S₁[ Nat] means ( $1 < p & $1 is prime );
consider X being Subset of NAT such that
A1: for q being Element of NAT holds
( q in X iff S₁[q] ) from SUBSET_1:sch 3();
take X ; :: thesis: for q being Nat holds
( q in X iff ( q < p & q is prime ) )
let q be Nat; :: thesis: ( q in X iff ( q < p & q is prime ) )
thus ( q in X implies ( q < p & q is prime ) ) by A1; :: thesis: ( q < p & q is prime implies q in X )
assume that
A2: q < p and
A3: q is prime ; :: thesis: q in X
q in NAT by ORDINAL1:def 12;
hence q in X by A1, A2, A3; :: thesis: verum