[STATEMENT]
lemma vrat_fpair_in_fproduct_vrat: "[a\<^sub>\<rat>, b\<^sub>\<rat>]\<^sub>\<circ> \<in>\<^sub>\<circ> \<rat>\<^sub>\<circ> ^\<^sub>\<times> 2\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a\<^sub>\<rat>, b\<^sub>\<rat>]\<^sub>\<circ> \<in>\<^sub>\<circ> \<rat>\<^sub>\<circ> ^\<^sub>\<times> 2\<^sub>\<nat>
[PROOF STEP]
by force