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

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

Hello,

Some time ago I asked about "Subset" versus "Element of
bool".  And then Grzegorz told me:

>It is better to repeat expandable definition after
>redefinition of "bool".

And I seem to remember that it helped then!  But now I'm looking
at it again, and I can't make it work anymore:

----------------------------------------------------------------
environ
 notation ZFMISC_1, SUBSET_1;
 constructors TARSKI, SUBSET_1;
 theorems ZFMISC_1;
 clusters SUBSET_1;
 requirements SUBSET;
begin

:: Subset of A -> Subset of B

definition
 let B be set;
 let A be Subset of B;
 redefine func bool A -> Subset of bool B;
 coherence by ZFMISC_1:79;
end;

definition
 let A be set;
 mode Subset of A is Element of bool A;
end;

for B being set, A being Subset of B, X being Subset of A holds
 X qua Subset of B is set;
::>  *116

for B being set, A being Subset of B, X being Element of bool A holds
 X qua Subset of B is set;

::>
::> 116: Invalid "qua"
----------------------------------------------------------------

I repeat the expandable definition of "Subset of" and still
it doesn't work?  What should I do to get the nice
transitivity of "Subset of"?  I'm very confused.

Freek