∀ {E : ℕ → Type u_1} [inst : (n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), DiscreteTopology (E n)] {x y : (n : ℕ) → E n}
  {s : Set ((n : ℕ) → E n)},
  IsClosed s →
    s.Nonempty →
      PiNat.longestPrefix x s < PiNat.firstDiff x y →
        x ∉ s → y ∉ s → PiNat.cylinder x (PiNat.longestPrefix x s) = PiNat.cylinder y (PiNat.longestPrefix y s)