theorem Th29: :: XTUPLE_0:29
for X, Y being set holds (proj2 X) \ (proj2 Y) c= proj2 (X \ Y)