theorem Th23: :: XTUPLE_0:23

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