theorem :: ENUMSET1:87

for x1, x2, x3 being set holds {x2,x1} \/ {x3,x1} = {x1,x2,x3}