∀ {α : Type u_1} {β : Type u_3} (m : α → β) (x : Set α) (σ : Type u_2) (F : CFilter (Set β) σ)
  (motive :
    x ∈
        { f := fun s => m ⁻¹' { σ := σ, F := F, eq := ⋯ }.F.f s, pt := { σ := σ, F := F, eq := ⋯ }.F.pt,
              inf := { σ := σ, F := F, eq := ⋯ }.F.inf, inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter.sets →
      Prop)
  (x_1 :
    x ∈
      { f := fun s => m ⁻¹' { σ := σ, F := F, eq := ⋯ }.F.f s, pt := { σ := σ, F := F, eq := ⋯ }.F.pt,
            inf := { σ := σ, F := F, eq := ⋯ }.F.inf, inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter.sets),
  (∀ (s : { σ := σ, F := F, eq := ⋯ }.σ)
      (h :
        { f := fun s => m ⁻¹' { σ := σ, F := F, eq := ⋯ }.F.f s, pt := { σ := σ, F := F, eq := ⋯ }.F.pt,
                inf := { σ := σ, F := F, eq := ⋯ }.F.inf, inf_le_left := ⋯, inf_le_right := ⋯ }.f
            s ⊆
          x),
      motive ⋯) →
    motive x_1