\begin{proposition}\label{in_irrefl}
For all sets $A$ we have $A\not\in A$.
\end{proposition}
\begin{proof}[Proof by \in-induction]
%Let $B$ be a set.
%Suppose $b\notin b$ for all $b\in B$.
%Suppose $B\in B$.
%But then
% $B\notin B$.
Straightforward.
\end{proof}