Re: [mizar] Strong Mizar wish: linking to consider

[Grzegorz Bancerek <bancerek@cs.shinshu-u.ac.jp>]

Freek Wiedijk wrote:

> >>   consider x such that
> >>  A1: P x and
> >>  A2: Q x by ...;
> >>   then R x by ...;
> 
> >>   1. "ex x st P x"
> >>   2. "P x & Q x"
> >>   3. "P x"
> >>   4. "Q x"
> I still think it should be 4!  If you want 2 you can write:
> 
>      consider x such that
>     A1: P x &
>         Q x by ...;
>      then R x by ...;

Obviously, 2 is better than 1 (ex x st P x & Q x) because 2 may be used
in every straightforward justification instead of 1. Not in scheme
justification,
but there we cannot use "then".
Definitely, 4 is better than 3.
The point 2 looks unnatural for me. On other hand it does not make much
sense:
if we want to refer only to P x (without Q x) in next justifications
we must have label A1 and we may use it to justify R x. If we do not
need
to refer to P x after R x we do not need to use "and".

But, sometime we must use "and". Namely, in collective assomption
     assume that
   A1:  alpha and
   A2:  beta
we may use definitional extension for single conjunct. We cannot do that
in regular cunjunction:  alpha & beta.

There is one more argument for 4. It is the simplest think to realize.
We must change only one flag in few places.

Grzegorz