∀ {R : Type u_1} [τR : TopologicalSpace R] [inst : Ring R] {A : Type u_3} [inst_1 : AddCommGroup A]
  [inst_2 : Module R A] [inst_3 : TopologicalSpace A] [IsModuleTopology R A] (S : Submodule R A),
  IsModuleTopology R (A ⧸ S)