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