[STATEMENT]
lemma l9_17:
  assumes "P Q OS A C" and
    "Bet A B C"
  shows "P Q OS A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P Q OS A B
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> P Q OS A B
 2. \<not> ?P \<Longrightarrow> P Q OS A B
[PROOF STEP]
assume "A = C"
[PROOF STATE]
proof (state)
this:
A = C

goal (2 subgoals):
 1. ?P \<Longrightarrow> P Q OS A B
 2. \<not> ?P \<Longrightarrow> P Q OS A B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A = C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A = C

goal (1 subgoal):
 1. P Q OS A B
[PROOF STEP]
using assms(1) assms(2) between_identity
[PROOF STATE]
proof (prove)
using this:
A = C
P Q OS A C
Bet A B C
\<forall>a b. Bet a b a \<longrightarrow> a = b

goal (1 subgoal):
 1. P Q OS A B
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P Q OS A B

goal (1 subgoal):
 1. A \<noteq> C \<Longrightarrow> P Q OS A B
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<noteq> C \<Longrightarrow> P Q OS A B
[PROOF STEP]
assume P1: "\<not> A = C"
[PROOF STATE]
proof (state)
this:
A \<noteq> C

goal (1 subgoal):
 1. A \<noteq> C \<Longrightarrow> P Q OS A B
[PROOF STEP]
obtain D where P2: "P Q TS A D \<and> P Q TS C D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>D. P Q TS A D \<and> P Q TS C D \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using OS_def assms(1)
[PROOF STATE]
proof (prove)
using this:
?A ?B OS ?P ?Q \<equiv> \<exists>R. ?A ?B TS ?P R \<and> ?A ?B TS ?Q R
P Q OS A C

goal (1 subgoal):
 1. (\<And>D. P Q TS A D \<and> P Q TS C D \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P Q TS A D \<and> P Q TS C D

goal (1 subgoal):
 1. A \<noteq> C \<Longrightarrow> P Q OS A B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P Q TS A D \<and> P Q TS C D
[PROOF STEP]
have P3: "P \<noteq> Q"
[PROOF STATE]
proof (prove)
using this:
P Q TS A D \<and> P Q TS C D

goal (1 subgoal):
 1. P \<noteq> Q
[PROOF STEP]
using ts_distincts
[PROOF STATE]
proof (prove)
using this:
P Q TS A D \<and> P Q TS C D
?A ?B TS ?P ?Q \<Longrightarrow> ?A \<noteq> ?B \<and> ?A \<noteq> ?P \<and> ?A \<noteq> ?Q \<and> ?B \<noteq> ?P \<and> ?B \<noteq> ?Q \<and> ?P \<noteq> ?Q

goal (1 subgoal):
 1. P \<noteq> Q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P \<noteq> Q

goal (1 subgoal):
 1. A \<noteq> C \<Longrightarrow> P Q OS A B
[PROOF STEP]
obtain X where P4: "Col X P Q \<and> Bet A X D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>X. Col X P Q \<and> Bet A X D \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using P2 TS_def
[PROOF STATE]
proof (prove)
using this:
P Q TS A D \<and> P Q TS C D
?A ?B TS ?P ?Q \<equiv> \<not> Col ?P ?A ?B \<and> \<not> Col ?Q ?A ?B \<and> (\<exists>T. Col T ?A ?B \<and> Bet ?P T ?Q)

goal (1 subgoal):
 1. (\<And>X. Col X P Q \<and> Bet A X D \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Col X P Q \<and> Bet A X D

goal (1 subgoal):
 1. A \<noteq> C \<Longrightarrow> P Q OS A B
[PROOF STEP]
obtain Y where P5: "Col Y P Q \<and> Bet C Y D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Y. Col Y P Q \<and> Bet C Y D \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using P2 TS_def
[PROOF STATE]
proof (prove)
using this:
P Q TS A D \<and> P Q TS C D
?A ?B TS ?P ?Q \<equiv> \<not> Col ?P ?A ?B \<and> \<not> Col ?Q ?A ?B \<and> (\<exists>T. Col T ?A ?B \<and> Bet ?P T ?Q)

goal (1 subgoal):
 1. (\<And>Y. Col Y P Q \<and> Bet C Y D \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Col Y P Q \<and> Bet C Y D

goal (1 subgoal):
 1. A \<noteq> C \<Longrightarrow> P Q OS A B
[PROOF STEP]
obtain T where P6: "Bet B T D \<and> Bet X T Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>T. Bet B T D \<and> Bet X T Y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using P4 P5 assms(2) l3_17
[PROOF STATE]
proof (prove)
using this:
Col X P Q \<and> Bet A X D
Col Y P Q \<and> Bet C Y D
Bet A B C
\<lbrakk>Bet ?A ?B ?C; Bet ?A' ?B' ?C; Bet ?A ?P ?A'\<rbrakk> \<Longrightarrow> \<exists>Q. Bet ?P Q ?C \<and> Bet ?B Q ?B'

goal (1 subgoal):
 1. (\<And>T. Bet B T D \<and> Bet X T Y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Bet B T D \<and> Bet X T Y

goal (1 subgoal):
 1. A \<noteq> C \<Longrightarrow> P Q OS A B
[PROOF STEP]
have P7: "P Q TS A D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P Q TS A D
[PROOF STEP]
by (simp add: P2)
[PROOF STATE]
proof (state)
this:
P Q TS A D

goal (1 subgoal):
 1. A \<noteq> C \<Longrightarrow> P Q OS A B
[PROOF STEP]
have "P Q TS B D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P Q TS B D
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P Q TS B D
[PROOF STEP]
have Q1: "\<not> Col B P Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Col B P Q
[PROOF STEP]
using assms(1) assms(2) one_side_chara
[PROOF STATE]
proof (prove)
using this:
P Q OS A C
Bet A B C
?P ?Q OS ?A ?B \<Longrightarrow> \<forall>X. Col X ?P ?Q \<longrightarrow> \<not> Bet ?A X ?B

goal (1 subgoal):
 1. \<not> Col B P Q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Col B P Q

goal (1 subgoal):
 1. P Q TS B D
[PROOF STEP]
have Q2: "\<not> Col D P Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Col D P Q
[PROOF STEP]
using P2 TS_def
[PROOF STATE]
proof (prove)
using this:
P Q TS A D \<and> P Q TS C D
?A ?B TS ?P ?Q \<equiv> \<not> Col ?P ?A ?B \<and> \<not> Col ?Q ?A ?B \<and> (\<exists>T. Col T ?A ?B \<and> Bet ?P T ?Q)

goal (1 subgoal):
 1. \<not> Col D P Q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Col D P Q

goal (1 subgoal):
 1. P Q TS B D
[PROOF STEP]
obtain T0 where "Col T0 P Q \<and> Bet B T0 D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>T0. Col T0 P Q \<and> Bet B T0 D \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>T0. Col T0 P Q \<and> Bet B T0 D \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
assume a1: "\<And>T0. Col T0 P Q \<and> Bet B T0 D \<Longrightarrow> thesis"
[PROOF STATE]
proof (state)
this:
Col ?T0.0 P Q \<and> Bet B ?T0.0 D \<Longrightarrow> thesis

goal (1 subgoal):
 1. (\<And>T0. Col T0 P Q \<and> Bet B T0 D \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain pp :: 'p where
        f2: "Bet B pp D \<and> Bet X pp Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>pp. Bet B pp D \<and> Bet X pp Y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>\<And>thesis. (\<And>T. Bet B T D \<and> Bet X T Y \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close>
[PROOF STATE]
proof (prove)
using this:
(\<And>T. Bet B T D \<and> Bet X T Y \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>pp. Bet B pp D \<and> Bet X pp Y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Bet B pp D \<and> Bet X pp Y

goal (1 subgoal):
 1. (\<And>T0. Col T0 P Q \<and> Bet B T0 D \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "Col P Q Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Col P Q Y
[PROOF STEP]
using Col_def P5
[PROOF STATE]
proof (prove)
using this:
Col ?A ?B ?C \<equiv> Bet ?A ?B ?C \<or> Bet ?B ?C ?A \<or> Bet ?C ?A ?B
Col Y P Q \<and> Bet C Y D

goal (1 subgoal):
 1. Col P Q Y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Col P Q Y

goal (1 subgoal):
 1. (\<And>T0. Col T0 P Q \<and> Bet B T0 D \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Col P Q Y
[PROOF STEP]
have "Y = X \<or> Col P Q pp"
[PROOF STATE]
proof (prove)
using this:
Col P Q Y

goal (1 subgoal):
 1. Y = X \<or> Col P Q pp
[PROOF STEP]
using f2 Col_def P4 colx
[PROOF STATE]
proof (prove)
using this:
Col P Q Y
Bet B pp D \<and> Bet X pp Y
Col ?A ?B ?C \<equiv> Bet ?A ?B ?C \<or> Bet ?B ?C ?A \<or> Bet ?C ?A ?B
Col X P Q \<and> Bet A X D
\<lbrakk>?A \<noteq> ?B; Col ?X ?Y ?A; Col ?X ?Y ?B; Col ?A ?B ?C\<rbrakk> \<Longrightarrow> Col ?X ?Y ?C

goal (1 subgoal):
 1. Y = X \<or> Col P Q pp
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Y = X \<or> Col P Q pp

goal (1 subgoal):
 1. (\<And>T0. Col T0 P Q \<and> Bet B T0 D \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Y = X \<or> Col P Q pp
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Y = X \<or> Col P Q pp

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using f2 a1
[PROOF STATE]
proof (prove)
using this:
Y = X \<or> Col P Q pp
Bet B pp D \<and> Bet X pp Y
Col ?T0.0 P Q \<and> Bet B ?T0.0 D \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (metis BetSEq BetS_def Col_def P4)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Col T0 P Q \<and> Bet B T0 D

goal (1 subgoal):
 1. P Q TS B D
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Col T0 P Q \<and> Bet B T0 D
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Col T0 P Q \<and> Bet B T0 D

goal (1 subgoal):
 1. P Q TS B D
[PROOF STEP]
using Q1 Q2
[PROOF STATE]
proof (prove)
using this:
Col T0 P Q \<and> Bet B T0 D
\<not> Col B P Q
\<not> Col D P Q

goal (1 subgoal):
 1. P Q TS B D
[PROOF STEP]
using TS_def
[PROOF STATE]
proof (prove)
using this:
Col T0 P Q \<and> Bet B T0 D
\<not> Col B P Q
\<not> Col D P Q
?A ?B TS ?P ?Q \<equiv> \<not> Col ?P ?A ?B \<and> \<not> Col ?Q ?A ?B \<and> (\<exists>T. Col T ?A ?B \<and> Bet ?P T ?Q)

goal (1 subgoal):
 1. P Q TS B D
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P Q TS B D

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P Q TS B D

goal (1 subgoal):
 1. A \<noteq> C \<Longrightarrow> P Q OS A B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P Q TS B D
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P Q TS B D

goal (1 subgoal):
 1. P Q OS A B
[PROOF STEP]
using P7
[PROOF STATE]
proof (prove)
using this:
P Q TS B D
P Q TS A D

goal (1 subgoal):
 1. P Q OS A B
[PROOF STEP]
using OS_def
[PROOF STATE]
proof (prove)
using this:
P Q TS B D
P Q TS A D
?A ?B OS ?P ?Q \<equiv> \<exists>R. ?A ?B TS ?P R \<and> ?A ?B TS ?Q R

goal (1 subgoal):
 1. P Q OS A B
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P Q OS A B

goal:
No subgoals!
[PROOF STEP]
qed