theorem Th78: :: COHSP_1:78

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