Is there intuitionistic proof that $B \setminus (B \setminus A) = A$ for any sets $A \subseteq B$? Let $A$ and $B$ be sets such that $A \subseteq B$. I am trying to investigate whether $A = B \setminus (B \setminus A)$. I am attempting to prove this by showing $(\forall x)[x \in A \Leftrightarrow x \in B \setminus (B \setminus A)]$. I was able to show that  $x \in A \Rightarrow x \in B \setminus (B \setminus A)$ without resorting to the LEM, but I could only solve the other direction using either the LEM itself or the elimination of double negations. Is this even provable in intuitionistic logic? If so, can I get some directions on how to solve it? Thanks in advance.
Here's how I solved the first direction: Let $x \in A$. Since $A \subseteq B$ then $x \in B$ and we must now show $x \notin B \setminus A$, i.e., $(x \in B \wedge x \notin A) \Rightarrow \perp$. We assume $x \in B$ and $x \notin A$ and reach a wanted contradiction since $x \in A$ by our hypothesis.
 A: In intuitionistic logic the powerset $\mathcal{P}(B)$ of a set $B$ generally forms a Heyting algebra. So your question then is whether for $A \in \mathcal{P}(B)$ we always have $\neg \neg A = A$. The answer to that is no: this equality does generally not hold in a Heyting algebra.
We can make things a bit more concrete, which might help with the insight why LEM is needed. In fact, if the equality you propose holds for all sets, then we have LEM. Let $P$ be any proposition, take $B = \{*\}$ to be a singleton and let $A = \{x \in B : P \vee \neg P\}$. By definition $* \in A$ if and only if $P \vee \neg P$. So we have $* \in B \setminus A$ if and only if $\neg(P \vee \neg P)$, and hence $* \in B \setminus (B \setminus A)$ if and only if $\neg \neg(P \vee \neg P)$. Now if we would have $A = B \setminus (B \setminus A)$, then $P \vee \neg P$ iff $* \in A$ iff $* \in B \setminus (B \setminus A)$ iff $\neg \neg(P \vee \neg P)$. Since $\neg \neg(P \vee \neg P)$ is a tautology, even in intuitionistic logic, we would conclude that $P \vee \neg P$. Since $P$ was arbitrary we thus have LEM.
