Re: [mizar] Isn't "Subset of" the same as "Element of bool"?

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

Dear Adam,

>I'm not sure whether it is exactly what you want, but I
>would write it as follows:
>
>definition
> let O be set;
> let A be Subset of O;
> mode Subset of A is Element of bool O;
>end;

But then Subset gets two different meanings!  I mean, this is
not done with a redefinition!  When I write "Subset of O" I
want it to "be" the Subset of O that I always already used.
Because maybe I want to apply theorems about Subset that are
already present.

?

Freek