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