consider A being set such that
A2: for x being object holds
( x in A iff ( x in dom f & S₂[x] ) ) from XBOOLE_0:sch 1();
take A ; :: thesis: for x being object holds
( x in A iff ( x in dom f & f . x <= a ) )
thus for x being object holds
( x in A iff ( x in dom f & f . x <= a ) ) by A2; :: thesis: verum