theorem :: XTUPLE_0:38

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