A generalization

The notion of an algebraic lattice is generalized as

definition
  let L be non empty reflexive RelStr;
  attr L is satisfying_axiom_K means                 :: WAYBEL_8:def 3 
    for x be Element of L holds x = sup compactbelow x;
end;

definition                                    :: DEFINITION 4.4, p. 85
  let L be non empty reflexive RelStr;
  attr L is algebraic means                          :: WAYBEL_8:def 4 
   (for x being Element of L 
      holds compactbelow x is non empty directed) &
    L is up-complete satisfying_axiom_K;
end;

Note the similarity between this definition and definitions of continuous lattices and complete lattices in Section . In all these cases, we use the property of existence of suprema of appropriate subsets rather than using the attribute complete. With this generalization we can treat algebraic lattices which are not complete, unlike the CCL-book which does not provide for such objects. Instead, the CCL-book proposes a separate definition of algebraic posets and semilattices in an exercise [25, Ch. I, 4.28, p. 94]. We find the MIZAR approach more convenient and we follow it also for the case of arithmetic lattices which we do not discuss here due to lack of space.