theorem :: EXCHSORT:3

for x, y being set st x nin y holds
(y \/ {x}) \ y = {x} by XBOOLE_1:88, ZFMISC_1:50;