Additional notation

The CCL-book very frequently uses the term $\downarrow\!\!x \cap K(L)$. While this term is not particularly complicated, we were afraid that we might run into typing problems as redefinitions $^{\:\alph{redefinitions}}$ are delicate constructs allowed only for functors and not for terms. Therefore, the following shorthand notation was introduced

definition
  let L be non empty reflexive RelStr,  x be Element of L;
  func compactbelow x -> Subset of L equals          :: WAYBEL_8:def 2 
    { y where y is Element of L: x >= y & y is compact };
end;

which substantially simplified further writing. The above definition employs the Fraenkel operator in its definiens. The Fraenkel operator is very convenient in definitions since we do not have to prove existence. However, using such a definition is rather tedious and thus a more convenient characterization of the defined notion is expressed as a theorem.

theorem                                                  :: WAYBEL_8:4 
for L be non empty reflexive RelStr, x, y be Element of L 
 holds y in compactbelow x iff x >= y & y is compact;

The original $\downarrow\!\!x \cap K(L)$ from the CCL-book is written as compactbelow x and the following theorem shows that they are equivalent.

theorem                                                  :: WAYBEL_8:5 
for L be non empty reflexive RelStr, x be Element of L holds 
  compactbelow x = downarrow x /\ the carrier of CompactSublatt L;