[mizar] Global choice

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

Dear Freek,

Freek Wiedijk wrote:

> because the "consider x"
> would give the fixed set, I suppose.

When I wrote that, according to Mizar semantics, such an 'x' is not
necessarily
  the fixed set
it was true. However, we may use
   set x = the fixed set
instead.

Then because
   consider x being set
is only shorthand for
   consider x being set such that not contradiction
the last may be eliminated from Mizar. The grammar becomes a bit
simpler.

Andrzej