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