Re: [mizar] [piotr@sedalia.cs.ualberta.ca: A request from W W Armstrong]

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

Piotr Rudnicki:

>	definition
>	  let X be set;
>	  cluster (B1) (B2) Subset-Family of X;
>	end;
>
>he got stuck and was totally confused.  The attributes and the type are
>earlier defined in the paper.  The source of his confusion was the word
>"definition" because what on Earth is being defined here.  Bill says that
>if instead of "definition" there was some other keyword, his confusion would
>probably be not as frustrating.

Yes, I've seen this frustration too.

I think this "cluster" thing really is a _theorem_ (but with
the system applying the theorem automatically all the time),
not a "definition":

  for X being set holds ex IT being Subset-Family of X st IT is (B1) (B2);

(I hope I got this right.)

Freek