let x, y be set ; :: thesis: union {{x},{y}} = {x,y}
thus union {{x},{y}} = {x} \/ {y} by Lm16
.= {x,y} by ENUMSET1:41 ; :: thesis: verum