theorem Th76: :: COHSP_1:76

for x, y being set
for z being object holds
( [z,1] in x U+ y iff z in x )