∀ {X : Type u_1} [t : TopologicalSpace X] [inst : T2Space X] (C : Set X) [inst_1 : Topology.CWComplex C] (E : Set X)
  (I : (n : ℕ) → Set (Topology.RelCWComplex.cell C n))
  (closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), Topology.RelCWComplex.closedCell n ↑i ⊆ E)
  (union : ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = E) (n : ℕ),
  (Topology.CWComplex.Subcomplex.mk' C E I closedCell_subset union).I n = I n