Clustering

[Christoph Schwarzweller <schwarzw@informatik.uni-tuebingen.de>]

Hi,

I have a problem when trying to cluster a function:

I used an attribute "add-closed"

    definition
    let L be non empty LoopStr,
        F be Subset of L;
    attr F is add-closed means
      for x, y being Element of L st x î F & y î F holds x+y î F;
     end;

and wanted to state the following cluster

     definition
     let L be non empty LoopStr,
          I,J be non empty Subset of L;
     cluster I ï J -> add-closed;
     end;

but I get that "add-closed"  is an "unknown attribute", although the
type of  I ï J seems to be correct, that is Mizar accepts
"for L be non empty 1-sorted,
       I,J be non empty Subset of L holds I ï J is Subset of R;"
in my environment.

Does anyone have an idea or a comment?
Thanks

Christoph