∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] (x b : X) {a y : X},
  x ⊓ y = a →
    x ≠ y → JordanHolderLattice.IsMaximal x b → JordanHolderLattice.IsMaximal y b → JordanHolderLattice.IsMaximal a y