theorem :: XTUPLE_0:46

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