theorem Th77: :: COHSP_1:77

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