theorem :: XBOOLE_1:92

for X being set holds X \+\ X = {} by Lm1;