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

goal (1 subgoal):
 1. finite (SP \<phi>)
[PROOF STEP]
by fastforce