theorem :: SETFAM_1:42

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