∀ {Γ : Type u_1} {R : Type u_2} (κ : Cardinal.{u_1}) [inst : PartialOrder Γ] [inst_1 : AddGroup R]
  [hκ : Fact (Cardinal.aleph0 ≤ κ)] {x : HahnSeries Γ R}, x ∈ HahnSeries.cardSuppLTAddSubgroup Γ R κ ↔ x.cardSupp < κ