defpred S₁[ Element of ] means $1 is atom ;
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 atom )
thus for x being Element of holds
( x in X iff x is atom ) by A1; :: thesis: verum