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