theorem Th8: :: XTUPLE_0:8

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