>>13794495By the definition we have which means so by transitivity is injective.
Moreover, any is contained in the image of .
If it were not, we would have an such that , but is the successor of , so there is so such .
All that is left to show the surjectivity of is to show that it is not bounded.
Suppose the contrary and let .
By definition of the supremum the predecessor of , say , lies in , so we have some such that , and thus
.
Likewise, the sucessor of also lies in the image of , so cannot be a supremum. Hence is unbounded.
