let X, Y be set ; :: thesis: union {X,Y,{} } = union {X,Y}
thus union {X,Y,{} } = union ({X,Y} \/ {{} }) by ENUMSET1:43
.= (union {X,Y}) \/ (union {{} }) by ZFMISC_1:96
.= (union {X,Y}) \/ {} by ZFMISC_1:31
.= union {X,Y} ; :: thesis: verum