[STATEMENT]
lemma at_within_interior:
  "NO_MATCH (UNIV::'a set) (S::'a::topological_space set) \<Longrightarrow> x \<in> interior S \<Longrightarrow> at x within S = at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>NO_MATCH UNIV S; x \<in> interior S\<rbrakk> \<Longrightarrow> at x within S = at x
[PROOF STEP]
by (rule at_within_interior)