Subset of compact elements

The CCL-book defines the subset $K(L)$ of all compact elements of a lattice $L$ and treats it as a set. The CCL-book does not make a clear distinction between a subset of a structure and a substructure of the structure. A better solution for the formalization seemed to be the introduction of a corresponding sublattice in WAYBEL_8 [39] as

  
definition 				      :: DEFINITION 4.1, p. 85
  let L be non empty reflexive RelStr;
  func CompactSublatt L -> strict full SubRelStr of L means
                                                     :: WAYBEL_8:def 1 
   for x being Element of L 
    holds x in the carrier of it iff x is compact;
end;

where full has the usual category theoretic meaning of restricting the internal relation to the carrier of the substructure. Where the CCL-book uses $K(L)$, we write

  the carrier of CompactSublatt L

which at the time of its introduction seemed a better solution. If we had introduced the following functor

  func COMPACT L -> Subset of L

to play the role of $K(L)$, then in many places we would have had to use expressions of the form

for K being SubRelStr st the carrier of K = COMPACT L holds ...

which do not read elegantly. It seems that using CompactSublatt L avoided this inconvenience and by introducing appropriate functorial $\mathrm{registrations}^{\:\alph{registrations}}$ for it, the mechanization of some reasoning steps became possible.

However, in hindsight it now seems that working with just a set and using MIZAR cluster mechanisms to carry the needed information could have been just as effective, if not better. With COMPACT defined above, we could have used the functor subrelstr (defined in YELLOW_0 [5] and applicable to a subset of a structure) which recovers the full substructure of its argument. In that case, instead of CompactSublatt L, we would have been working with subrelstr COMPACT L and instead of the carrier of the former, we would have written just COMPACT L. Another possibility would have been to define a host of term adjective registrations for subrelstr COMPACT L as the type of this term carries all the information about L. However, that would be impossible for the carrier of CompactSublatt L as its type is just set. An MML revision may change the current solution.