theorem :: SYSREL:16

for X, Y being set holds (id (X \ Y)) \ (id X) = {} by Th15, XBOOLE_1:37;