Re: Linking facts emerging from consider/given?

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Markus Wenzel wrote:

>
>   consider x such that x = y; then y = x;
>   :: consider/given may not be used with linking!?
>   ::>  *164                             *164
>
> This restriction looks quite arbitrary for me.  Is there any good reason
> why this is so?  The key feature of consider/given versus other statements
> that produce facts appears to be that multiple results may emerge
> simultaneaously.  So I would suspect that this might be *some* reason for
> this slightly odd end.  Is there any better explanation according to the
> Mizar semantics?

Let us look to more realistic example:

 assume y in rng f;
 then consider x such that
w1:  x in dom f and
w2: y = f.x by FUNCT_1:11;

There are at least three sentences that may be considered as "the last
sentence" (linking is to the last sentence)

   ex x st x in dom f  & y=f.x
   x in dom f & y = f.x
   y = f.x

(actually in some implementations the last generated sentence while processing
was "x in dom f" :-))

I believe allowing "then " in such a situation would be misleading.

Andrzej