This is a short one: . Solution:

The way is clear: we have to suppose , and finally see that, in that case, is true. The trick: is always true, whether we suppose or not.

We must use implication introduction, but this needs a hypothesis, and, some lines below, the result of the supposition. Only then we can close the hypothesis.

So after opening it (line 2), we must do something to write down that . Since we already have it written in line 1, we simply put again and justify it with , which means ``I copied this from line 1''. The is for iteration.

We now fulfill the requirements to apply the rule, so we apply it, closing the subdemonstration, and we've ended.

Daniel Clemente Laboreo 2005-05-17