# Successor is Less than Successor/Sufficient Condition

This page has been identified as a candidate for refactoring of basic complexity.In particular: See parent pageUntil this has been finished, please leave
`{{Refactor}}` in the code.
Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$.To discuss this page in more detail, feel free to use the talk page.When this work has been completed, you may remove this instance of `{{Refactor}}` from the code. |

## Theorem

Let $x$ and $y$ be ordinals and let $x^+$ denote the successor set of $x$.

Let $x^+ \in y^+$.

Then:

- $x \in y$

## Proof 1

Suppose $y^+ \in x^+$.

By the definition of successor, $y^+ \in x \lor y^+ = x$.

Suppose $y^+ = x$.

By Ordinal is Less than Successor, $y \in x$.

Suppose $y^+ \in x$.

By Ordinal is Less than Successor, $y \in y^+$.

By Ordinal is Transitive, $y \in x$.

$\blacksquare$

## Proof 2

First note that by Successor Set of Ordinal is Ordinal, $x^+$ and $y^+$ are ordinals.

Let $x^+ \in y^+$.

Then since $y^+$ is transitive, $x^+ \subseteq y^+$.

Thus $x \in y$ or $x = y$.

If $x = y$ then $x^+ \in x^+$, contradicting Ordinal is not Element of Itself.

Thus $x \in y$.

$\blacksquare$