theorem :: XBOOLE_1:45

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