theorem Th75: :: COHSP_1:75

for x, y, z being set st z in x U+ y holds
( z = [(z `1),(z `2)] & ( ( z `2 = 1 & z `1 in x ) or ( z `2 = 2 & z `1 in y ) ) )