[STATEMENT]
lemma analz_Un_implSecureSet_aux_3:
  "Enc_keys_clean (G \<union> H) \<Longrightarrow>
  analz (implSecureSet_aux Ag G \<union> H) \<subseteq> synth (analz (G \<union> H)) \<union> -payload"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Enc_keys_clean (G \<union> H) \<Longrightarrow> analz (implSecureSet_aux Ag G \<union> H) \<subseteq> synth (analz (G \<union> H)) \<union> - payload
[PROOF STEP]
by (rule subset_trans [OF analz_Un_implSecureSet_aux_2], auto)