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