theorem Th25: :: XTUPLE_0:25

for X, Y being set holds (proj1 X) \ (proj1 Y) c= proj1 (X \ Y)