Topology on Over X is subcanonical if the base is

We show that if J is subcanonical, then also J.over X is subcanonical.

theorem CategoryTheory.GrothendieckTopology.subcanonical_over {C : Type u_1} [Category.{v_1, u_1} C] (J : GrothendieckTopology C) [J.Subcanonical] (X : C) : (J.over X).Subcanonical