theorem Th35: :: XTUPLE_0:35

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