[STATEMENT]
lemma \<pi>_subset_elem_trans: 
  assumes Y: "Y \<subseteq> \<pi> k T X"
  assumes z: "z \<in> \<pi> k T Y"
  shows "z \<in>  \<pi> k T X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<in> \<pi> k T X
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z \<in> \<pi> k T X
[PROOF STEP]
from Y
[PROOF STATE]
proof (chain)
picking this:
Y \<subseteq> \<pi> k T X
[PROOF STEP]
have "\<pi> k T Y \<subseteq> \<pi> k T (\<pi> k T X)"
[PROOF STATE]
proof (prove)
using this:
Y \<subseteq> \<pi> k T X

goal (1 subgoal):
 1. \<pi> k T Y \<subseteq> \<pi> k T (\<pi> k T X)
[PROOF STEP]
by (simp add: monoD mono_\<pi>)
[PROOF STATE]
proof (state)
this:
\<pi> k T Y \<subseteq> \<pi> k T (\<pi> k T X)

goal (1 subgoal):
 1. z \<in> \<pi> k T X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<pi> k T Y \<subseteq> \<pi> k T (\<pi> k T X)
[PROOF STEP]
have "\<pi> k T Y \<subseteq> \<pi> k T X"
[PROOF STATE]
proof (prove)
using this:
\<pi> k T Y \<subseteq> \<pi> k T (\<pi> k T X)

goal (1 subgoal):
 1. \<pi> k T Y \<subseteq> \<pi> k T X
[PROOF STEP]
using \<pi>_idempotent
[PROOF STATE]
proof (prove)
using this:
\<pi> k T Y \<subseteq> \<pi> k T (\<pi> k T X)
\<pi> ?k ?T (\<pi> ?k ?T ?I) = \<pi> ?k ?T ?I

goal (1 subgoal):
 1. \<pi> k T Y \<subseteq> \<pi> k T X
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<pi> k T Y \<subseteq> \<pi> k T X

goal (1 subgoal):
 1. z \<in> \<pi> k T X
[PROOF STEP]
with z
[PROOF STATE]
proof (chain)
picking this:
z \<in> \<pi> k T Y
\<pi> k T Y \<subseteq> \<pi> k T X
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
z \<in> \<pi> k T Y
\<pi> k T Y \<subseteq> \<pi> k T X

goal (1 subgoal):
 1. z \<in> \<pi> k T X
[PROOF STEP]
using contra_subsetD
[PROOF STATE]
proof (prove)
using this:
z \<in> \<pi> k T Y
\<pi> k T Y \<subseteq> \<pi> k T X
\<lbrakk>?A \<subseteq> ?B; ?c \<notin> ?B\<rbrakk> \<Longrightarrow> ?c \<notin> ?A

goal (1 subgoal):
 1. z \<in> \<pi> k T X
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
z \<in> \<pi> k T X

goal:
No subgoals!
[PROOF STEP]
qed