definition restrict_uniformity ≝
λC:uniform_space.λX:C→Prop.
{U:C square → Prop| (U ⊆ {x:C square|X (fst x) ∧ X(snd x)}) ∧ us_unifbase C U}.
definition restrict_uniformity ≝
λC:uniform_space.λX:C→Prop.
{U:C square → Prop| (U ⊆ {x:C square|X (fst x) ∧ X(snd x)}) ∧ us_unifbase C U}.