theorem Th6: :: CIRCCMB2:6

for X being without_pairs set
for Y being Relation holds X \ Y = X