let x, y be object ; :: thesis: union {{x},{y}} = {x,y}
thus union {{x},{y}} = {x} \/ {y} by Lm15
.= {x,y} by ENUMSET1:1 ; :: thesis: verum