defpred S₁[ set ] means for x being set st x in dom Ch & Ch . x = y holds
$1 in F . x;
consider I being set such that
A1: for z being set holds
( z in I iff ( z in union (rng F) & S₁[z] ) ) from XBOOLE_0:sch 1();
I c= union (rng F)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in I or x in union (rng F) )
assume x in I ; :: thesis: x in union (rng F)
hence x in union (rng F) by A1; :: thesis: verum

end;

then reconsider I = I as Subset of (union (rng F)) ;
take I ; :: thesis: for z being set holds
( z in I iff ( z in union (rng F) & ( for x being set st x in dom Ch & Ch . x = y holds
z in F . x ) ) )
thus for z being set holds
( z in I iff ( z in union (rng F) & ( for x being set st x in dom Ch & Ch . x = y holds
z in F . x ) ) ) by A1; :: thesis: verum