theorem :: MBOOLEAN:24
for x, y being object
for I being set holds union (I --> {{x},{y}}) = I --> {x,y}