∀ {α : Type u_4} {inst : TopologicalSpace α} {carrier : Set α} {isIrreducible' : IsIrreducible carrier}
  {isClosed' : IsClosed carrier} {carrier_1 : Set α} {isIrreducible'_1 : IsIrreducible carrier_1}
  {isClosed'_1 : IsClosed carrier_1},
  { carrier := carrier, isIrreducible' := isIrreducible', isClosed' := isClosed' } =
      { carrier := carrier_1, isIrreducible' := isIrreducible'_1, isClosed' := isClosed'_1 } →
    carrier = carrier_1