[STATEMENT]
lemma vcard_vlepoll: "vcard A \<le> vcard B \<longleftrightarrow> A \<lesssim>\<^sub>\<circ> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (vcard A \<subseteq>\<^sub>\<circ> vcard B) = (A \<lesssim>\<^sub>\<circ> B)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vcard A \<subseteq>\<^sub>\<circ> vcard B \<Longrightarrow> A \<lesssim>\<^sub>\<circ> B
 2. A \<lesssim>\<^sub>\<circ> B \<Longrightarrow> vcard A \<subseteq>\<^sub>\<circ> vcard B
[PROOF STEP]
assume "vcard A \<le> vcard B"
[PROOF STATE]
proof (state)
this:
vcard A \<subseteq>\<^sub>\<circ> vcard B

goal (2 subgoals):
 1. vcard A \<subseteq>\<^sub>\<circ> vcard B \<Longrightarrow> A \<lesssim>\<^sub>\<circ> B
 2. A \<lesssim>\<^sub>\<circ> B \<Longrightarrow> vcard A \<subseteq>\<^sub>\<circ> vcard B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
vcard A \<subseteq>\<^sub>\<circ> vcard B

goal (2 subgoals):
 1. vcard A \<subseteq>\<^sub>\<circ> vcard B \<Longrightarrow> A \<lesssim>\<^sub>\<circ> B
 2. A \<lesssim>\<^sub>\<circ> B \<Longrightarrow> vcard A \<subseteq>\<^sub>\<circ> vcard B
[PROOF STEP]
have "vcard A \<approx>\<^sub>\<circ> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard A \<approx>\<^sub>\<circ> A
[PROOF STEP]
by (rule cardinal_eqpoll)
[PROOF STATE]
proof (state)
this:
vcard A \<approx>\<^sub>\<circ> A

goal (2 subgoals):
 1. vcard A \<subseteq>\<^sub>\<circ> vcard B \<Longrightarrow> A \<lesssim>\<^sub>\<circ> B
 2. A \<lesssim>\<^sub>\<circ> B \<Longrightarrow> vcard A \<subseteq>\<^sub>\<circ> vcard B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
vcard A \<approx>\<^sub>\<circ> A

goal (2 subgoals):
 1. vcard A \<subseteq>\<^sub>\<circ> vcard B \<Longrightarrow> A \<lesssim>\<^sub>\<circ> B
 2. A \<lesssim>\<^sub>\<circ> B \<Longrightarrow> vcard A \<subseteq>\<^sub>\<circ> vcard B
[PROOF STEP]
have "vcard B \<approx>\<^sub>\<circ> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard B \<approx>\<^sub>\<circ> B
[PROOF STEP]
by (rule cardinal_eqpoll)
[PROOF STATE]
proof (state)
this:
vcard B \<approx>\<^sub>\<circ> B

goal (2 subgoals):
 1. vcard A \<subseteq>\<^sub>\<circ> vcard B \<Longrightarrow> A \<lesssim>\<^sub>\<circ> B
 2. A \<lesssim>\<^sub>\<circ> B \<Longrightarrow> vcard A \<subseteq>\<^sub>\<circ> vcard B
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
vcard A \<subseteq>\<^sub>\<circ> vcard B
vcard A \<approx>\<^sub>\<circ> A
vcard B \<approx>\<^sub>\<circ> B
[PROOF STEP]
show "A \<lesssim>\<^sub>\<circ> B"
[PROOF STATE]
proof (prove)
using this:
vcard A \<subseteq>\<^sub>\<circ> vcard B
vcard A \<approx>\<^sub>\<circ> A
vcard B \<approx>\<^sub>\<circ> B

goal (1 subgoal):
 1. A \<lesssim>\<^sub>\<circ> B
[PROOF STEP]
by (meson eqpoll_sym lepoll_trans1 lepoll_trans2 vlepoll_vsubset)
[PROOF STATE]
proof (state)
this:
A \<lesssim>\<^sub>\<circ> B

goal (1 subgoal):
 1. A \<lesssim>\<^sub>\<circ> B \<Longrightarrow> vcard A \<subseteq>\<^sub>\<circ> vcard B
[PROOF STEP]
qed (simp add: lepoll_imp_Card_le)