theorem Th31: :: XTUPLE_0:31

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