theorem :: XBOOLE_1:38

for X, Y being set st X c= Y \ X holds
X = {}