[STATEMENT]
lemma vintersection_intersection: "A \<inter>\<^sub>\<circ> B = set (elts A \<inter> elts B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<inter>\<^sub>\<circ> B = set (elts A \<inter> elts B)
[PROOF STEP]
unfolding inf_V_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (elts A \<inter> elts B) = set (elts A \<inter> elts B)
[PROOF STEP]
by simp