  Recently, a novel fixed point operation has been introduced over certain
non-monotonic functions between stratified complete lattices and used to give
semantics to logic programs with negation and boolean context-free grammars. We
prove that this new operation satisfies `the standard' identities of fixed
point operations as described by the axioms of iteration theories. We also
study this new fixed point operation in connection with lambda-abstraction.
