Successor set

context	$X$
definiendum	${\mathrm{succ}}\ X \equiv X \cup \{X\}$

$X\in {\mathrm{succ}}\ X$
$({\mathrm{succ}}\ X={\mathrm{succ}}\ Y)\Rightarrow (X=Y)$
$(Y\in {\mathrm{succ}}\ X)\Leftrightarrow (Y=X\lor Y=\{X\})$
$X\neq {\mathrm{succ}}\ X$