[STATEMENT]
theorem hyp2_axiom11:
  "\<forall> X Y. (\<exists> a. \<forall> x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y)
  \<longrightarrow> (\<exists> b. \<forall> x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>X Y. (\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y) \<longrightarrow> (\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)
[PROOF STEP]
proof (rule allI)+
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>X Y. (\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y) \<longrightarrow> (\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)
[PROOF STEP]
fix X Y :: "hyp2 set"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>X Y. (\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y) \<longrightarrow> (\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)
[PROOF STEP]
show "(\<exists> a. \<forall> x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y)
    \<longrightarrow> (\<exists> b. \<forall> x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y) \<longrightarrow> (\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> (\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y) \<longrightarrow> (\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)
 2. \<not> ?P \<Longrightarrow> (\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y) \<longrightarrow> (\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)
[PROOF STEP]
assume "X = {} \<or> Y = {}"
[PROOF STATE]
proof (state)
this:
X = {} \<or> Y = {}

goal (2 subgoals):
 1. ?P \<Longrightarrow> (\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y) \<longrightarrow> (\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)
 2. \<not> ?P \<Longrightarrow> (\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y) \<longrightarrow> (\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)
[PROOF STEP]
thus "(\<exists> a. \<forall> x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y)
      \<longrightarrow> (\<exists> b. \<forall> x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)"
[PROOF STATE]
proof (prove)
using this:
X = {} \<or> Y = {}

goal (1 subgoal):
 1. (\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y) \<longrightarrow> (\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y) \<longrightarrow> (\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)

goal (1 subgoal):
 1. \<not> (X = {} \<or> Y = {}) \<Longrightarrow> (\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y) \<longrightarrow> (\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (X = {} \<or> Y = {}) \<Longrightarrow> (\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y) \<longrightarrow> (\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)
[PROOF STEP]
assume "\<not> (X = {} \<or> Y = {})"
[PROOF STATE]
proof (state)
this:
\<not> (X = {} \<or> Y = {})

goal (1 subgoal):
 1. \<not> (X = {} \<or> Y = {}) \<Longrightarrow> (\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y) \<longrightarrow> (\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)
[PROOF STEP]
hence "X \<noteq> {}" and "Y \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
\<not> (X = {} \<or> Y = {})

goal (1 subgoal):
 1. X \<noteq> {} &&& Y \<noteq> {}
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
X \<noteq> {}
Y \<noteq> {}

goal (1 subgoal):
 1. \<not> (X = {} \<or> Y = {}) \<Longrightarrow> (\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y) \<longrightarrow> (\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
X \<noteq> {}
Y \<noteq> {}
[PROOF STEP]
obtain w and z where "w \<in> X" and "z \<in> Y"
[PROOF STATE]
proof (prove)
using this:
X \<noteq> {}
Y \<noteq> {}

goal (1 subgoal):
 1. (\<And>w z. \<lbrakk>w \<in> X; z \<in> Y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w \<in> X
z \<in> Y

goal (1 subgoal):
 1. \<not> (X = {} \<or> Y = {}) \<Longrightarrow> (\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y) \<longrightarrow> (\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)
[PROOF STEP]
show "(\<exists> a. \<forall> x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y)
      \<longrightarrow> (\<exists> b. \<forall> x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y) \<longrightarrow> (\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y \<Longrightarrow> \<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y
[PROOF STEP]
assume "\<exists> a. \<forall> x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y"
[PROOF STATE]
proof (state)
this:
\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y

goal (1 subgoal):
 1. \<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y \<Longrightarrow> \<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y
[PROOF STEP]
obtain a where "\<forall> x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y"
[PROOF STATE]
proof (prove)
using this:
\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y

goal (1 subgoal):
 1. (\<And>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y

goal (1 subgoal):
 1. \<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y \<Longrightarrow> \<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y
[PROOF STEP]
let ?cX = "hyp2_rep ` X"
        and ?cY = "hyp2_rep ` Y"
        and ?ca = "hyp2_rep a"
        and ?cw = "hyp2_rep w"
        and ?cz = "hyp2_rep z"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y \<Longrightarrow> \<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y
[PROOF STEP]
from \<open>\<forall> x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y
[PROOF STEP]
have "\<forall> cx cy. cx \<in> ?cX \<and> cy \<in> ?cY \<longrightarrow> B\<^sub>\<real> ?ca cx cy"
[PROOF STATE]
proof (prove)
using this:
\<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y

goal (1 subgoal):
 1. \<forall>cx cy. cx \<in> hyp2_rep ` X \<and> cy \<in> hyp2_rep ` Y \<longrightarrow> B\<^sub>\<real> hyp2_rep a cx cy
[PROOF STEP]
by (unfold real_hyp2_B_def) auto
[PROOF STATE]
proof (state)
this:
\<forall>cx cy. cx \<in> hyp2_rep ` X \<and> cy \<in> hyp2_rep ` Y \<longrightarrow> B\<^sub>\<real> hyp2_rep a cx cy

goal (1 subgoal):
 1. \<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y \<Longrightarrow> \<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y
[PROOF STEP]
with real_euclid.A11' [of ?cX ?cY ?ca]
[PROOF STATE]
proof (chain)
picking this:
\<forall>x y. x \<in> hyp2_rep ` X \<and> y \<in> hyp2_rep ` Y \<longrightarrow> B\<^sub>\<real> hyp2_rep a x y \<Longrightarrow> \<exists>b. \<forall>x y. x \<in> hyp2_rep ` X \<and> y \<in> hyp2_rep ` Y \<longrightarrow> B\<^sub>\<real> x b y
\<forall>cx cy. cx \<in> hyp2_rep ` X \<and> cy \<in> hyp2_rep ` Y \<longrightarrow> B\<^sub>\<real> hyp2_rep a cx cy
[PROOF STEP]
obtain cb where "\<forall> cx cy. cx \<in> ?cX \<and> cy \<in> ?cY \<longrightarrow> B\<^sub>\<real> cx cb cy"
[PROOF STATE]
proof (prove)
using this:
\<forall>x y. x \<in> hyp2_rep ` X \<and> y \<in> hyp2_rep ` Y \<longrightarrow> B\<^sub>\<real> hyp2_rep a x y \<Longrightarrow> \<exists>b. \<forall>x y. x \<in> hyp2_rep ` X \<and> y \<in> hyp2_rep ` Y \<longrightarrow> B\<^sub>\<real> x b y
\<forall>cx cy. cx \<in> hyp2_rep ` X \<and> cy \<in> hyp2_rep ` Y \<longrightarrow> B\<^sub>\<real> hyp2_rep a cx cy

goal (1 subgoal):
 1. (\<And>cb. \<forall>cx cy. cx \<in> hyp2_rep ` X \<and> cy \<in> hyp2_rep ` Y \<longrightarrow> B\<^sub>\<real> cx cb cy \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>cx cy. cx \<in> hyp2_rep ` X \<and> cy \<in> hyp2_rep ` Y \<longrightarrow> B\<^sub>\<real> cx cb cy

goal (1 subgoal):
 1. \<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y \<Longrightarrow> \<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y
[PROOF STEP]
with \<open>w \<in> X\<close> and \<open>z \<in> Y\<close>
[PROOF STATE]
proof (chain)
picking this:
w \<in> X
z \<in> Y
\<forall>cx cy. cx \<in> hyp2_rep ` X \<and> cy \<in> hyp2_rep ` Y \<longrightarrow> B\<^sub>\<real> cx cb cy
[PROOF STEP]
have "B\<^sub>\<real> ?cw cb ?cz"
[PROOF STATE]
proof (prove)
using this:
w \<in> X
z \<in> Y
\<forall>cx cy. cx \<in> hyp2_rep ` X \<and> cy \<in> hyp2_rep ` Y \<longrightarrow> B\<^sub>\<real> cx cb cy

goal (1 subgoal):
 1. B\<^sub>\<real> hyp2_rep w cb hyp2_rep z
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
B\<^sub>\<real> hyp2_rep w cb hyp2_rep z

goal (1 subgoal):
 1. \<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y \<Longrightarrow> \<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y
[PROOF STEP]
hence "hyp2_rep (hyp2_abs cb) = cb" (is "hyp2_rep ?b = cb")
[PROOF STATE]
proof (prove)
using this:
B\<^sub>\<real> hyp2_rep w cb hyp2_rep z

goal (1 subgoal):
 1. hyp2_rep (hyp2_abs cb) = cb
[PROOF STEP]
by (rule between_inverse)
[PROOF STATE]
proof (state)
this:
hyp2_rep (hyp2_abs cb) = cb

goal (1 subgoal):
 1. \<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y \<Longrightarrow> \<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y
[PROOF STEP]
with \<open>\<forall> cx cy. cx \<in> ?cX \<and> cy \<in> ?cY \<longrightarrow> B\<^sub>\<real> cx cb cy\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>cx cy. cx \<in> hyp2_rep ` X \<and> cy \<in> hyp2_rep ` Y \<longrightarrow> B\<^sub>\<real> cx cb cy
hyp2_rep (hyp2_abs cb) = cb
[PROOF STEP]
have "\<forall> x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x ?b y"
[PROOF STATE]
proof (prove)
using this:
\<forall>cx cy. cx \<in> hyp2_rep ` X \<and> cy \<in> hyp2_rep ` Y \<longrightarrow> B\<^sub>\<real> cx cb cy
hyp2_rep (hyp2_abs cb) = cb

goal (1 subgoal):
 1. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x hyp2_abs cb y
[PROOF STEP]
by (unfold real_hyp2_B_def) simp
[PROOF STATE]
proof (state)
this:
\<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x hyp2_abs cb y

goal (1 subgoal):
 1. \<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y \<Longrightarrow> \<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y
[PROOF STEP]
thus "\<exists> b. \<forall> x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y"
[PROOF STATE]
proof (prove)
using this:
\<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x hyp2_abs cb y

goal (1 subgoal):
 1. \<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y
[PROOF STEP]
by (rule exI)
[PROOF STATE]
proof (state)
this:
\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y) \<longrightarrow> (\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y) \<longrightarrow> (\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)

goal:
No subgoals!
[PROOF STEP]
qed