theorem :: ZFMISC_1:75

for X, Y being set holds union {X,Y} = X \/ Y by Lm15;