defpred S₁[ object ] 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 object holds
( z in I iff ( z in union (rng F) & S₁[z] ) ) from XBOOLE_0:sch 1();
I c= union (rng F) by A1;
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