:: deftheorem Def2 defines Intersection CARD_FIN:def 2 :
for F, Ch being Function
for y being object
for b₄ being Subset of (union (rng F)) holds
( b₄ = Intersection (F,Ch,y) iff for z being set holds
( z in b₄ iff ( z in union (rng F) & ( for x being set st x in dom Ch & Ch . x = y holds
z in F . x ) ) ) );