diff options
Diffstat (limited to 'test/phase5/exact-induction-nested.tex')
| -rw-r--r-- | test/phase5/exact-induction-nested.tex | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/test/phase5/exact-induction-nested.tex b/test/phase5/exact-induction-nested.tex index 060a787..e9c5402 100644 --- a/test/phase5/exact-induction-nested.tex +++ b/test/phase5/exact-induction-nested.tex @@ -1,10 +1,11 @@ \begin{proposition}\label{phase5_nested_set_induction} - For all sets $x$ we have $x = x$. + Let $A$ be a set. + Then for all $x\in A$ such that $x\neq A$ we have $x = x$. \end{proposition} \begin{proof} - Fix $x$. - Show $x = x$. - \begin{subproof}[Proof by \in-induction on $x$] + Show for all $x\in A$ such that $x\neq A$ we have $x = x$. + \begin{subproof}[Proof by \in-induction] + Assume $x\in A$ and $x\neq A$. Follows by assumption. \end{subproof} Follows by assumption. |