∀ {X : Type u_1} [inst : TopologicalSpace X] [PrespectralSpace X] (Z : Set X),
  ¬IsPreirreducible Z →
    ∃ A B, IsClosed A ∧ IsClosed B ∧ IsCompact Aᶜ ∧ IsCompact Bᶜ ∧ Z ⊆ A ∪ B ∧ (Z ∩ Aᶜ).Nonempty ∧ (Z ∩ Bᶜ).Nonempty