[STATEMENT]
theorem mk_alt_consistency_subset: \<open>C \<subseteq> mk_alt_consistency C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<subseteq> mk_alt_consistency C
[PROOF STEP]
unfolding mk_alt_consistency_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<subseteq> {S. \<exists>f. psubst f ` S \<in> C}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> C \<Longrightarrow> x \<in> {S. \<exists>f. psubst f ` S \<in> C}
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> C \<Longrightarrow> x \<in> {S. \<exists>f. psubst f ` S \<in> C}
[PROOF STEP]
assume \<open>x \<in> C\<close>
[PROOF STATE]
proof (state)
this:
x \<in> C

goal (1 subgoal):
 1. \<And>x. x \<in> C \<Longrightarrow> x \<in> {S. \<exists>f. psubst f ` S \<in> C}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> C
[PROOF STEP]
have \<open>psubst id ` x \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> C

goal (1 subgoal):
 1. psubst id ` x \<in> C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
psubst id ` x \<in> C

goal (1 subgoal):
 1. \<And>x. x \<in> C \<Longrightarrow> x \<in> {S. \<exists>f. psubst f ` S \<in> C}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
psubst id ` x \<in> C
[PROOF STEP]
have \<open>(\<exists>f. psubst f ` x \<in> C)\<close>
[PROOF STATE]
proof (prove)
using this:
psubst id ` x \<in> C

goal (1 subgoal):
 1. \<exists>f. psubst f ` x \<in> C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>f. psubst f ` x \<in> C

goal (1 subgoal):
 1. \<And>x. x \<in> C \<Longrightarrow> x \<in> {S. \<exists>f. psubst f ` S \<in> C}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>f. psubst f ` x \<in> C
[PROOF STEP]
show \<open>x \<in> {S. \<exists>f. psubst f ` S \<in> C}\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>f. psubst f ` x \<in> C

goal (1 subgoal):
 1. x \<in> {S. \<exists>f. psubst f ` S \<in> C}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> {S. \<exists>f. psubst f ` S \<in> C}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subset_in_close:
  assumes \<open>S \<subseteq> S'\<close>
  shows \<open>S' \<union> x \<in> C \<longrightarrow> S \<union> x \<in> close C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S' \<union> x \<in> C \<longrightarrow> S \<union> x \<in> close C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. S' \<union> x \<in> C \<longrightarrow> S \<union> x \<in> close C
[PROOF STEP]
have \<open>S' \<union> x \<in> close C \<longrightarrow> S \<union> x \<in> close C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S' \<union> x \<in> close C \<longrightarrow> S \<union> x \<in> close C
[PROOF STEP]
unfolding close_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S' \<union> x \<in> {S. Bex C ((\<subseteq>) S)} \<longrightarrow> S \<union> x \<in> {S. Bex C ((\<subseteq>) S)}
[PROOF STEP]
using \<open>S \<subseteq> S'\<close>
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> S'

goal (1 subgoal):
 1. S' \<union> x \<in> {S. Bex C ((\<subseteq>) S)} \<longrightarrow> S \<union> x \<in> {S. Bex C ((\<subseteq>) S)}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S' \<union> x \<in> close C \<longrightarrow> S \<union> x \<in> close C

goal (1 subgoal):
 1. S' \<union> x \<in> C \<longrightarrow> S \<union> x \<in> close C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S' \<union> x \<in> close C \<longrightarrow> S \<union> x \<in> close C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
S' \<union> x \<in> close C \<longrightarrow> S \<union> x \<in> close C

goal (1 subgoal):
 1. S' \<union> x \<in> C \<longrightarrow> S \<union> x \<in> close C
[PROOF STEP]
unfolding close_def
[PROOF STATE]
proof (prove)
using this:
S' \<union> x \<in> {S. Bex C ((\<subseteq>) S)} \<longrightarrow> S \<union> x \<in> {S. Bex C ((\<subseteq>) S)}

goal (1 subgoal):
 1. S' \<union> x \<in> C \<longrightarrow> S \<union> x \<in> {S. Bex C ((\<subseteq>) S)}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S' \<union> x \<in> C \<longrightarrow> S \<union> x \<in> close C

goal:
No subgoals!
[PROOF STEP]
qed