theorem Th1: :: GLIB_009:1

for X, Y being set st Y c= X holds
X \ (X \ Y) = Y