∀ {α : Type u_2} {inst : TopologicalSpace α} {carrier : Set α} {is_open' : IsOpen carrier} {carrier_1 : Set α}
  {is_open'_1 : IsOpen carrier_1},
  { carrier := carrier, is_open' := is_open' } = { carrier := carrier_1, is_open' := is_open'_1 } → carrier = carrier_1