theorem :: SETFAM_1:25

for X, SFY being set holds X /\ (union SFY) = union (INTERSECTION ({X},SFY))