{P : Type u_1} →
  {L : Type u_2} →
    [inst : Membership P L] →
      (∀ (l : L), ∃ p, p ∉ l) →
        (∀ (p : P), ∃ l, p ∉ l) →
          (∀ {p₁ p₂ : P} {l₁ l₂ : L}, p₁ ∈ l₁ → p₂ ∈ l₁ → p₁ ∈ l₂ → p₂ ∈ l₂ → p₁ = p₂ ∨ l₁ = l₂) →
            (mkLine : {p₁ p₂ : P} → p₁ ≠ p₂ → L) →
              (∀ {p₁ p₂ : P} (h : p₁ ≠ p₂), p₁ ∈ mkLine h ∧ p₂ ∈ mkLine h) → Configuration.HasLines P L