theorem Th9: :: XTUPLE_0:9

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