defpred S₁[ object ] means f . $1 <> 0. S;
consider X being set such that
A1: for x being object holds
( x in X iff ( x in dom f & S₁[x] ) ) from XBOOLE_0:sch 1();
take X ; :: thesis: for x being set holds
( x in X iff ( x in dom f & f . x <> 0. S ) )
let x be set ; :: thesis: ( x in X iff ( x in dom f & f . x <> 0. S ) )
thus ( x in X iff ( x in dom f & f . x <> 0. S ) ) by A1; :: thesis: verum