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

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

Dear Josef,

>Note that tha "bool" in (D2) is the original "bool" (let's
>call it "bool#1"), not the redefined ("bool#2") from (D1),

I see!  I completely missed this.  Thanks for explaining
this, I hope that now I can make this behave like I want.

>To get bool#2 here, you would have to write in (D2):
>let B be set;
>let A be Subset of B; 
>instead (i.e. what Adam suggests).

But Adam did then define Subset of A as Element of bool B, I
think.  That had confused me.

>If you do in Emacs: 
>Mizar->Const. Explanations->Verbosity->translated formula, 
>and Shift-mouse3 on the final semicolon after processing,
>this one expands to:

At some point (quite long ago) I stopped upgrading the Mizar
mode.  It threw a window at me, and I didn't like that, so I
kept the old version from then on (probably I could turn
these extra windows off, but at that time I didn't want to
spend time on it.)

But maybe you can show all these niceties to me at MKM :-)

And thanks again to Grzegorz and Adam and you for helping me
understand this!

Freek