theorem Th17: :: XTUPLE_0:17

for X, Y being set st X c= Y holds
proj2_4 X c= proj2_4 Y