defpred S₁[ Element of ] means $1 is prime ;
consider X being Subset of such that
A1: for x being Element of holds
( x in X iff S₁[x] ) from SUBSET_1:sch 3();
take X ; :: thesis: for x being Element of holds
( x in X iff x is prime )
thus for x being Element of holds
( x in X iff x is prime ) by A1; :: thesis: verum