[STATEMENT]
lemma closed_Collect_imp: "open {x. P x} \<Longrightarrow> closed {x. Q x} \<Longrightarrow> closed {x. P x \<longrightarrow> Q x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>open {x. P x}; closed {x. Q x}\<rbrakk> \<Longrightarrow> closed {x. P x \<longrightarrow> Q x}
[PROOF STEP]
unfolding imp_conv_disj
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>open {x. P x}; closed {x. Q x}\<rbrakk> \<Longrightarrow> closed {x. \<not> P x \<or> Q x}
[PROOF STEP]
by (intro closed_Collect_disj closed_Collect_neg)