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