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