diff options
Diffstat (limited to 'library/set/cons.tex')
| -rw-r--r-- | library/set/cons.tex | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/library/set/cons.tex b/library/set/cons.tex index 5972ebe..4ab1041 100644 --- a/library/set/cons.tex +++ b/library/set/cons.tex @@ -111,7 +111,11 @@ Then $\cons{a}{A\setminus\{a\}} = A$. \end{proposition} \begin{proof} - Follows by \cref{cons_iff,setext,setminus}. + We have for all $x\in\cons{a}{A\setminus\{a\}}$ we have $x\in A$ + by \cref{cons_iff,setminus}. + We have for all $x\in A$ we have $x\in\cons{a}{A\setminus\{a\}}$ + by \cref{cons_iff,setminus}. + Follows by set extensionality. \end{proof} \begin{proposition}\label{cons_idempotent} |