You can't finish the deduction inside a subdemonstration. The last line can't have any vertical line to the left.

The reason is that everything from inside the subdemonstration is valid only when the supposition is really true, and what the original problem asks is to prove that the formula at the right of the is always true.

Here's a sample of what can be tried by someone very astute who wants to prove :

We supposed , and also . In that case, of course it's true that , but only in that case. We can't affirm to anyone that is always true. So, we should start closing the two demonstrations (first the inner one, and then the outer one) to extract some conclusion which is always valid.

Neither could we do that iteration thing at line 4. I already explained this before.

Daniel Clemente Laboreo 2005-05-17