Re: [mizar] Reference distances?

[Freek Wiedijk <freek@cs.ru.nl>]

Hi Artur,

>Maybe my answer is out of your question, but in an "ideal"
>case such a proof should not appear.

Yes, that's a different issue :-)

>It should look like:
>
>proof
>  assume that
>A1: ... and
>A2: ...;
>  ex ... st ... & ... by ...;
>  hence ... by ...;
>end;
>
>where you have two labels and two justifications.

But even then the justifications don't match the labels!

And really you have _four_ places where you _could_ have
labels in your variant of the proof, as you could also label
the "ex ...", and the statement after the "hence".

Freek