[STATEMENT]
lemma atMost_Int_atLeast: "{..\<le>\<^sub>an} \<inter> {n\<le>\<^sub>a..} = {n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {..\<le>\<^sub>an} \<inter> {n\<le>\<^sub>a..} = {n}
[PROOF STEP]
unfolding ray_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> UNIV. x \<le>\<^sub>a n} \<inter> {x \<in> UNIV. n \<le>\<^sub>a x} = {n}
[PROOF STEP]
by (auto simp: eq_iff)