consider A being set such that
A4: 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 & a <= f . x ) )
thus for x being object holds
( x in A iff ( x in dom f & a <= f . x ) ) by A4; :: thesis: verum