Double complement law proof I'm having difficulty proving that $S-(S-A) = A$ iff $A \subseteq S$, where "$-$" is the set difference.
For the "only if" part, I found that I can prove that 
$S \subset A \Longrightarrow S-(S-A) \neq A$
by letting $x$ be an element in $A$ which is not in $S$. Then I show that $S-(S-A)$ does not contains $x$ from which it follows that $S-(S-A) \neq A$.
For the "if" part, even though it is conceptually very intuitive, I can't find a way to make a formal proof.
 A: $A\subset S$ is not the negation of $A\subseteq S$: you must also consider the possibility that there is some $x\in A\setminus S$. It’s not hard to see that that also implies that $S\setminus(S\setminus A)\ne A$, but you do have to consider the case if you take this approach to proving the theorem. You could prove this direction more easily by simply observing that $S\setminus(S\setminus A)\subseteq S$, so if $S\setminus(S\setminus A)=A$, then $A\subseteq S$.
For the other direction, you could try to prove directly that if $A\subseteq S$, then $S\setminus(S\setminus A)=A$. Suppose that $x\in A$; then $x\in S$, and $x\notin S\setminus A$, so $x\in S\setminus(S\setminus A)$, and therefore $A\subseteq S\setminus(S\setminus A)$. Now suppose that $x\in S\setminus(S\setminus A)$. Then $x\in S$ and $x\notin S\setminus A$, so ... ?
A: I would do this with some simple calculations.  First, we simplify $\;S - (S - A)\;$: for all $\;x\;$,
\begin{align}
& x \in S - (S - A) \\
\equiv & \;\;\;\;\;\text{"definition of $\;-\;$, twice"} \\
& x \in S \;\land\; \lnot (x \in S \;\land\; \lnot (x \in A)) \\
\equiv & \;\;\;\;\;\text{"logic: DeMorgan"} \\
& x \in S \;\land\; (\lnot(x \in S) \;\lor\; x \in A) \\
\equiv & \;\;\;\;\;\text{"logic: use $\;x \in S\;$ on other side of $\;\land\;$"} \\
& x \in S \;\land\; (\lnot(\text{true}) \;\lor\; x \in A) \\
\equiv & \;\;\;\;\;\text{"logic: simplify"} \\
& x \in S \;\land\; x \in A \\
\end{align}
Therefore
\begin{align}
& S - (S - A) = A \\
\equiv & \;\;\;\;\;\text{"set extensionality; the above calculation"} \\
& \langle \forall x :: x \in S \land x \in A \;\equiv\; x \in A \rangle \\
\equiv & \;\;\;\;\;\text{"logic: $\;p \equiv p \land q\;$ is one of the ways to write $\;p \Rightarrow q\;$"} \\
& \langle \forall x :: x \in A \;\Rightarrow\; x \in S \rangle \\
\equiv & \;\;\;\;\;\text{"definition of $\;\subseteq\;$"} \\
& A \subseteq S \\
\end{align}
This completes the proof.
