theorem :: MBOOLEAN:21

for I being set holds union (EmptyMS I) = EmptyMS I