One of the most natural ways to record derivations formally is called, well, Natural Deduction. Each inference rule is written as a line with assumptions written above and one conclusion below the line. Also, there are scoping rules: some assumptions are available up to some point, after which the are closed. E.g., in proving A -> B, we assume A and may use it to derive B. Then A is closed and we obtain A -> B. After that, A can no longer be used.
Existential elimination rule (using an assumption of the form has the following form.
Here the assumption is closed by the last line. It corresponds to regular mathematical practice: if we know , but don't know what exactly is, we could prove that implies for any . Then we would know .
In text form, it is convenient to write derivations showing scoping explicitly. The existential elimination rule is written as follows.
This means that, having , we temporarily introduce an assumption , deduce from it, and then close . The result is a derivation of from .
Using this, the proof about < can be written as follows.