theorem Th8: :: CIRCCMB2:8

for X, Z being set
for Y being Relation st Z c= Y & X \ Z is without_pairs holds
X \ Y = X \ Z