theorem Th11: :: XTUPLE_0:11

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