theorem Th80: :: COHSP_1:80

for x1, y1, x2, y2 being set holds
( x1 U+ y1 = x2 U+ y2 iff ( x1 = x2 & y1 = y2 ) ) by Th78;