let x, y be object ; :: thesis: for X being set holds
( [:{x,y},X:] = [:{x},X:] \/ [:{y},X:] & [:X,{x,y}:] = [:X,{x}:] \/ [:X,{y}:] )
let 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 Th96; :: thesis: verum