theorem Th10: :: XTUPLE_0:10

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