defpred S₁[ set ] means f . $1 <> 0. S;
consider B being Subset of X such that
A1: for x being Element of X holds
( x in B iff S₁[x] ) from SUBSET_1:sch 3();
take B ; :: thesis: for x being Element of X holds
( x in B iff f . x <> 0. S )
thus for x being Element of X holds
( x in B iff f . x <> 0. S ) by A1; :: thesis: verum