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

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

Hi,

Another question...

I'm trying this:

  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;

  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've been looking, but I couldn't find this redefinition
elsewhere (did I miss it?)

But the main question: why doesn't this work when X is
Subset of A, but it _does_ work when X is Element of bool A?
I thought that both were the same!  Because in SUBSET_1 it says:

  definition let X;
   mode Subset of X is Element of bool X;
  end;

?

Excuse me if this is another silly question.

Freek