∀ {R : Type u_2} {A : Type u_1} [inst : CommRing R] [inst_1 : NonUnitalNonAssocRing A] [inst_2 : Module R A]
  (S T : NonUnitalSubalgebra R A),
  (fun S => S.toNonUnitalSubring) S = (fun S => S.toNonUnitalSubring) T → ∀ (x : A), x ∈ S ↔ x ∈ T