150theorem exists_logicRealization_of_distinction 151 (K : Type u) [Nonempty K] (h : ∃ x y : K, x ≠ y) : 152 Nonempty (LogicRealization.{u, 0}) := by
proof body
Term-mode proof.
153 classical 154 rcases h with ⟨x, y, hxy⟩ 155 exact ⟨logicRealizationOfDistinction K x y hxy⟩ 156 157/-- A more precise version retaining the chosen points. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.