theorem Th1: :: ENUMSET1:1

for x1, x2 being object holds {x1,x2} = {x1} \/ {x2}