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