theorem :: XTUPLE_0:26

for X, Y being set holds (proj1 X) \+\ (proj1 Y) c= proj1 (X \+\ Y)