Geach-Kaplan sentence

Stream: maths

[Bulhwi Cha]

Do you think my formalization of the Geach-Kaplan sentence is correct?

import Mathlib.Data.Set.Basic

opaque Human : Type
opaque isCritic : Human → Prop
opaque Admires : Human → Human → Prop
infix:55 " admires " => Admires

-- the Geach-Kaplan sentence: "some critics admire only one another"
def GKS : Prop := ∃ isSomeCritic : Human → Prop, (∃ x : Human, isSomeCritic x)
∧ (∀ x : Human, isSomeCritic x → isCritic x ∧ (∃ y : Human, x admires y)
  ∧ ∀ y : Human, x admires y → isSomeCritic y ∧ x ≠ y)

-- restate the proposition `GKS` by using `Set`
def GKS' : Prop := ∃ someCritics : Set Human, (∃ x : Human, x ∈ someCritics)
∧ (∀ x : Human, x ∈ someCritics → isCritic x ∧ (∃ y : Human, x admires y)
  ∧ ∀ y : Human, x admires y → y ∈ someCritics ∧ x ≠ y)

-- the above two definitions are equivalent
example : GKS ↔ GKS' := Iff.refl GKS

[Bulhwi Cha]

Should I keep ∃ y : Human, x admires y in the definitions?

[Bulhwi Cha]

I think GKS requires that "at least two critics admire each other," so I'll leave it as it is.