theorem Th16: :: XTUPLE_0:16

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