[STATEMENT]
lemma finite_subset[trans]: "A \<subseteq> B \<Longrightarrow> finite B \<Longrightarrow> finite A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<subseteq> B; finite B\<rbrakk> \<Longrightarrow> finite A
[PROOF STEP]
using finite_subset
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. \<lbrakk>A \<subseteq> B; finite B\<rbrakk> \<Longrightarrow> finite A
[PROOF STEP]
by this