MatchingLogic.EntryIII.Lindenbaum

theorem MatchingLogic.locConsistent_extend_isMCS {S : Signature} {Var : Type} [DecidableEq Var] {Gamma : Set (Pattern S Var)} (hGamma : LocConsistent Gamma) : ∃ (Delta : Set (Pattern S Var)), Gamma ⊆ Delta ∧ IsMCS Delta

Every locally consistent pattern set is included in a maximal locally consistent set. This is the non-witnessed Zorn part of the source's Lindenbaum construction.