theorem :: XTUPLE_0:42

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