let X1, X2, X3 be set ; :: thesis: union {X1,X2,X3} = (X1 \/ X2) \/ X3
thus union {X1,X2,X3} = union ({X1,X2} \/ {X3}) by ENUMSET1:3
.= (union {X1,X2}) \/ (union {X3}) by ZFMISC_1:78
.= (X1 \/ X2) \/ (union {X3}) by ZFMISC_1:75
.= (X1 \/ X2) \/ X3 ; :: thesis: verum