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