theorem :: ZFMISC_1:83

for A, B being set st ( for X, Y being set st X <> Y & X in A \/ B & Y in A \/ B holds
X misses Y ) holds
union (A /\ B) = (union A) /\ (union B)