[STATEMENT]
lemma col_cop_perp2__pars_bis:
  assumes "\<not> Col A B P" and
    "Col C D P" and
    "Coplanar A B C D" and
    "P Perp2 A B C D"
  shows "A B ParStrict C D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A B ParStrict C D
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A B ParStrict C D
[PROOF STEP]
obtain X Y where P1: "Col P X Y \<and> X Y Perp A B \<and> X Y Perp C D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>X Y. Col P X Y \<and> X Y Perp A B \<and> X Y Perp C D \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Perp2_def assms(4)
[PROOF STATE]
proof (prove)
using this:
?P Perp2 ?A ?B ?C ?D \<equiv> \<exists>X Y. Col ?P X Y \<and> X Y Perp ?A ?B \<and> X Y Perp ?C ?D
P Perp2 A B C D

goal (1 subgoal):
 1. (\<And>X Y. Col P X Y \<and> X Y Perp A B \<and> X Y Perp C D \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Col P X Y \<and> X Y Perp A B \<and> X Y Perp C D

goal (1 subgoal):
 1. A B ParStrict C D
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Col P X Y \<and> X Y Perp A B \<and> X Y Perp C D
[PROOF STEP]
have "Col X Y P"
[PROOF STATE]
proof (prove)
using this:
Col P X Y \<and> X Y Perp A B \<and> X Y Perp C D

goal (1 subgoal):
 1. Col X Y P
[PROOF STEP]
using Col_perm
[PROOF STATE]
proof (prove)
using this:
Col P X Y \<and> X Y Perp A B \<and> X Y Perp C D
Col ?A ?B ?C \<Longrightarrow> Col ?A ?B ?C \<and> Col ?A ?C ?B \<and> Col ?B ?A ?C \<and> Col ?B ?C ?A \<and> Col ?C ?A ?B \<and> Col ?C ?B ?A

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

goal (1 subgoal):
 1. A B ParStrict C D
[PROOF STEP]
obtain Q where "X \<noteq> Q \<and> Y \<noteq> Q \<and> P \<noteq> Q \<and> Col X Y Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Q. X \<noteq> Q \<and> Y \<noteq> Q \<and> P \<noteq> Q \<and> Col X Y Q \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>Col X Y P\<close> diff_col_ex3
[PROOF STATE]
proof (prove)
using this:
Col X Y P
Col ?A ?B ?C \<Longrightarrow> \<exists>D. ?A \<noteq> D \<and> ?B \<noteq> D \<and> ?C \<noteq> D \<and> Col ?A ?B D

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

goal (1 subgoal):
 1. A B ParStrict C D
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
X \<noteq> Q \<and> Y \<noteq> Q \<and> P \<noteq> Q \<and> Col X Y Q

goal (1 subgoal):
 1. A B ParStrict C D
[PROOF STEP]
by (smt P1 Perp_perm assms(1) assms(2) assms(3) col_cop_perp2_pars col_permutation_1 col_transitivity_2 not_col_distincts perp_col4 perp_distinct)
[PROOF STATE]
proof (state)
this:
A B ParStrict C D

goal:
No subgoals!
[PROOF STEP]
qed