theorem Th74: :: COHSP_1:74

for x being set holds
( x U+ {} = [:x,{1}:] & {} U+ x = [:x,{2}:] )