TopologicalSpace.PositiveCompacts.Icc01 =
  { carrier := Set.Icc 0 1, isCompact' := TopologicalSpace.PositiveCompacts.Icc01._proof_1,
    interior_nonempty' := TopologicalSpace.PositiveCompacts.Icc01._proof_3 }