theorem :: BOOLE:1

for X being set holds X \/ {} = X