theorem :: ZFMISC_1:109

for x, y being object
for X being set holds
( [:{x,y},X:] = [:{x},X:] \/ [:{y},X:] & [:X,{x,y}:] = [:X,{x}:] \/ [:X,{y}:] )