:: deftheorem defines U+ COHSP_1:def 22 :
for x, y being set holds x U+ y = Union (disjoin <*x,y*>);