∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M]
  (s : UpperSet (MulArchimedeanClass M)) {x : M},
  x ∈ (MulArchimedeanClass.subsemigroup s).carrier → x⁻¹ ∈ (MulArchimedeanClass.subsemigroup s).carrier