[STATEMENT]
lemma relative_to_subset:
   "S \<subseteq> T \<and> P S \<Longrightarrow> (P relative_to T) S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<subseteq> T \<and> P S \<Longrightarrow> (P relative_to T) S
[PROOF STEP]
unfolding relative_to_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<subseteq> T \<and> P S \<Longrightarrow> \<exists>U. P U \<and> T \<inter> U = S
[PROOF STEP]
by auto