∀ (R : Type u) [inst : CommSemiring R] {A : Type u} [inst_1 : Semiring A] [inst_2 : Algebra R A] (s : Set A),
  Cardinal.mk ↥(Algebra.adjoin R s) ≤ max (max (Cardinal.mk R) (Cardinal.mk ↑s)) Cardinal.aleph0