theorem Th1: :: DILWORTH:1

for X, Y, x being set st not x in X holds
X \ (Y \/ {x}) = X \ Y