Linking facts emerging from consider/given?

[Markus Wenzel <wenzelm@informatik.tu-muenchen.de>]

According to some Mizar documentation which I do not remember now, local
results emerging from "consider" or "given" may not be linked (via "then"
or "hence").  Indeed this is what Mizar has to say about that situation:

  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?


	Markus

-------------------------------------------------------------------
Institut für Informatik, TU München, http://www.in.tum.de/~wenzelm/
--- <>< -----------------------------------------------------------