theorem Th27: :: XTUPLE_0:27

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