theorem :: XTUPLE_0:34

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