[STATEMENT]
lemma tiny_semicategories_vsubset_Vset: 
  "set {\<CC>. tiny_semicategory \<alpha> \<CC>} \<subseteq>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZFC_in_HOL.set {\<CC>. tiny_semicategory \<alpha> \<CC>} \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (rule vsubsetI) (simp add: tiny_semicategory.tiny_smc_in_Vset)