let x, y, X be set ; :: thesis: ( [:{x,y},X:] = [:{x},X:] \/ [:{y},X:] & [:X,{x,y}:] = [:X,{x}:] \/ [:X,{y}:] )
{x,y} = {x} \/ {y} by ENUMSET1:1;
hence ( [:{x,y},X:] = [:{x},X:] \/ [:{y},X:] & [:X,{x,y}:] = [:X,{x}:] \/ [:X,{y}:] ) by Th120; :: thesis: verum