let x1, x2, x3, x4 be set ; :: thesis: ({x1} \/ {x2}) \/ {x3,x4} = {x3,x1,x2,x4}
({x1} \/ {x2}) \/ {x3,x4} = {x1,x2} \/ {x3,x4} by ENUMSET1:1
.= {x1,x2,x3,x4} by ENUMSET1:5
.= {x3,x2,x1,x4} by ENUMSET1:71
.= {x3} \/ {x2,x1,x4} by ENUMSET1:4
.= {x3} \/ {x1,x2,x4} by ENUMSET1:58
.= {x3,x1,x2,x4} by ENUMSET1:4 ;
hence ({x1} \/ {x2}) \/ {x3,x4} = {x3,x1,x2,x4} ; :: thesis: verum