In Boolean algebras the properties of the implication operation can be mode
led by a so-called implication algebra that itself can be considered as a j
oin-semi lattice with 1 whose principal filters are Boolean algebras. This
situation is generalized from Boolean algebras to orthomodular lattices.