[STATEMENT]
lemma symm_closure_of_preorder_is_trans:
  fixes Rel :: "('a \<times> 'a) set"
  assumes condA: "\<forall>a b c. (a, b) \<in> Rel \<and> (c, b) \<in> Rel \<and> (a, c) \<notin> Rel
                  \<longrightarrow> (b, a) \<in> Rel \<or> (b, c) \<in> Rel"
      and condB: "\<forall>a b c. (a, b) \<in> Rel \<and> (a, c) \<in> Rel \<and> (b, c) \<notin> Rel
                  \<longrightarrow> (b, a) \<in> Rel \<or> (c, a) \<in> Rel"
      and reflR: "refl Rel"
      and tranR: "trans Rel"
  shows "trans (symcl Rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trans (symcl Rel)
[PROOF STEP]
unfolding trans_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y z. (x, y) \<in> symcl Rel \<longrightarrow> (y, z) \<in> symcl Rel \<longrightarrow> (x, z) \<in> symcl Rel
[PROOF STEP]
proof clarify
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y z. (x, y) \<in> symcl Rel \<and> (y, z) \<in> symcl Rel \<Longrightarrow> (x, z) \<in> symcl Rel
[PROOF STEP]
fix a b c
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y z. (x, y) \<in> symcl Rel \<and> (y, z) \<in> symcl Rel \<Longrightarrow> (x, z) \<in> symcl Rel
[PROOF STEP]
have "\<lbrakk>(a, b) \<in> Rel; (b, c) \<in> Rel\<rbrakk> \<Longrightarrow> (a, c) \<in> symcl Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a, b) \<in> Rel \<and> (b, c) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (a, b) \<in> Rel \<and> (b, c) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
assume "(a, b) \<in> Rel" and "(b, c) \<in> Rel"
[PROOF STATE]
proof (state)
this:
(a, b) \<in> Rel
(b, c) \<in> Rel

goal (1 subgoal):
 1. (a, b) \<in> Rel \<and> (b, c) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
with tranR
[PROOF STATE]
proof (chain)
picking this:
trans Rel
(a, b) \<in> Rel
(b, c) \<in> Rel
[PROOF STEP]
have "(a, c) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
trans Rel
(a, b) \<in> Rel
(b, c) \<in> Rel

goal (1 subgoal):
 1. (a, c) \<in> Rel
[PROOF STEP]
unfolding trans_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x y z. (x, y) \<in> Rel \<longrightarrow> (y, z) \<in> Rel \<longrightarrow> (x, z) \<in> Rel
(a, b) \<in> Rel
(b, c) \<in> Rel

goal (1 subgoal):
 1. (a, c) \<in> Rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(a, c) \<in> Rel

goal (1 subgoal):
 1. (a, b) \<in> Rel \<and> (b, c) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
thus "(a, c) \<in> symcl Rel"
[PROOF STATE]
proof (prove)
using this:
(a, c) \<in> Rel

goal (1 subgoal):
 1. (a, c) \<in> symcl Rel
[PROOF STEP]
by (simp add: symcl_def)
[PROOF STATE]
proof (state)
this:
(a, c) \<in> symcl Rel

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(a, b) \<in> Rel \<and> (b, c) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel

goal (1 subgoal):
 1. \<And>x y z. (x, y) \<in> symcl Rel \<and> (y, z) \<in> symcl Rel \<Longrightarrow> (x, z) \<in> symcl Rel
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(a, b) \<in> Rel \<and> (b, c) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel

goal (1 subgoal):
 1. \<And>x y z. (x, y) \<in> symcl Rel \<and> (y, z) \<in> symcl Rel \<Longrightarrow> (x, z) \<in> symcl Rel
[PROOF STEP]
have "\<lbrakk>(a, b) \<in> Rel; (c, b) \<in> Rel; (a, c) \<notin> Rel\<rbrakk> \<Longrightarrow> (a, c) \<in> symcl Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a, b) \<in> Rel \<and> (c, b) \<in> Rel \<and> (a, c) \<notin> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (a, b) \<in> Rel \<and> (c, b) \<in> Rel \<and> (a, c) \<notin> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
assume A1: "(a, b) \<in> Rel" and A2: "(c, b) \<in> Rel" and "(a, c) \<notin> Rel"
[PROOF STATE]
proof (state)
this:
(a, b) \<in> Rel
(c, b) \<in> Rel
(a, c) \<notin> Rel

goal (1 subgoal):
 1. (a, b) \<in> Rel \<and> (c, b) \<in> Rel \<and> (a, c) \<notin> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
with condA
[PROOF STATE]
proof (chain)
picking this:
\<forall>a b c. (a, b) \<in> Rel \<and> (c, b) \<in> Rel \<and> (a, c) \<notin> Rel \<longrightarrow> (b, a) \<in> Rel \<or> (b, c) \<in> Rel
(a, b) \<in> Rel
(c, b) \<in> Rel
(a, c) \<notin> Rel
[PROOF STEP]
have "(b, a) \<in> Rel \<or> (b, c) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<forall>a b c. (a, b) \<in> Rel \<and> (c, b) \<in> Rel \<and> (a, c) \<notin> Rel \<longrightarrow> (b, a) \<in> Rel \<or> (b, c) \<in> Rel
(a, b) \<in> Rel
(c, b) \<in> Rel
(a, c) \<notin> Rel

goal (1 subgoal):
 1. (b, a) \<in> Rel \<or> (b, c) \<in> Rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(b, a) \<in> Rel \<or> (b, c) \<in> Rel

goal (1 subgoal):
 1. (a, b) \<in> Rel \<and> (c, b) \<in> Rel \<and> (a, c) \<notin> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
thus "(a, c) \<in> symcl Rel"
[PROOF STATE]
proof (prove)
using this:
(b, a) \<in> Rel \<or> (b, c) \<in> Rel

goal (1 subgoal):
 1. (a, c) \<in> symcl Rel
[PROOF STEP]
proof auto
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (b, a) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
 2. (b, c) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
assume "(b, a) \<in> Rel"
[PROOF STATE]
proof (state)
this:
(b, a) \<in> Rel

goal (2 subgoals):
 1. (b, a) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
 2. (b, c) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
with A2 tranR
[PROOF STATE]
proof (chain)
picking this:
(c, b) \<in> Rel
trans Rel
(b, a) \<in> Rel
[PROOF STEP]
have "(c, a) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(c, b) \<in> Rel
trans Rel
(b, a) \<in> Rel

goal (1 subgoal):
 1. (c, a) \<in> Rel
[PROOF STEP]
unfolding trans_def
[PROOF STATE]
proof (prove)
using this:
(c, b) \<in> Rel
\<forall>x y z. (x, y) \<in> Rel \<longrightarrow> (y, z) \<in> Rel \<longrightarrow> (x, z) \<in> Rel
(b, a) \<in> Rel

goal (1 subgoal):
 1. (c, a) \<in> Rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(c, a) \<in> Rel

goal (2 subgoals):
 1. (b, a) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
 2. (b, c) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
thus "(a, c) \<in> symcl Rel"
[PROOF STATE]
proof (prove)
using this:
(c, a) \<in> Rel

goal (1 subgoal):
 1. (a, c) \<in> symcl Rel
[PROOF STEP]
by (simp add: symcl_def)
[PROOF STATE]
proof (state)
this:
(a, c) \<in> symcl Rel

goal (1 subgoal):
 1. (b, c) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (b, c) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
assume "(b, c) \<in> Rel"
[PROOF STATE]
proof (state)
this:
(b, c) \<in> Rel

goal (1 subgoal):
 1. (b, c) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
with A1 tranR
[PROOF STATE]
proof (chain)
picking this:
(a, b) \<in> Rel
trans Rel
(b, c) \<in> Rel
[PROOF STEP]
have "(a, c) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> Rel
trans Rel
(b, c) \<in> Rel

goal (1 subgoal):
 1. (a, c) \<in> Rel
[PROOF STEP]
unfolding trans_def
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> Rel
\<forall>x y z. (x, y) \<in> Rel \<longrightarrow> (y, z) \<in> Rel \<longrightarrow> (x, z) \<in> Rel
(b, c) \<in> Rel

goal (1 subgoal):
 1. (a, c) \<in> Rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(a, c) \<in> Rel

goal (1 subgoal):
 1. (b, c) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
thus "(a, c) \<in> symcl Rel"
[PROOF STATE]
proof (prove)
using this:
(a, c) \<in> Rel

goal (1 subgoal):
 1. (a, c) \<in> symcl Rel
[PROOF STEP]
by (simp add: symcl_def)
[PROOF STATE]
proof (state)
this:
(a, c) \<in> symcl Rel

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(a, c) \<in> symcl Rel

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(a, b) \<in> Rel \<and> (c, b) \<in> Rel \<and> (a, c) \<notin> Rel \<Longrightarrow> (a, c) \<in> symcl Rel

goal (1 subgoal):
 1. \<And>x y z. (x, y) \<in> symcl Rel \<and> (y, z) \<in> symcl Rel \<Longrightarrow> (x, z) \<in> symcl Rel
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(a, b) \<in> Rel \<and> (c, b) \<in> Rel \<and> (a, c) \<notin> Rel \<Longrightarrow> (a, c) \<in> symcl Rel

goal (1 subgoal):
 1. \<And>x y z. (x, y) \<in> symcl Rel \<and> (y, z) \<in> symcl Rel \<Longrightarrow> (x, z) \<in> symcl Rel
[PROOF STEP]
have "\<lbrakk>(b, a) \<in> Rel; (b, c) \<in> Rel; (a, c) \<notin> Rel\<rbrakk> \<Longrightarrow> (a, c) \<in> symcl Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b, a) \<in> Rel \<and> (b, c) \<in> Rel \<and> (a, c) \<notin> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (b, a) \<in> Rel \<and> (b, c) \<in> Rel \<and> (a, c) \<notin> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
assume B1: "(b, a) \<in> Rel" and B2: "(b, c) \<in> Rel" and "(a, c) \<notin> Rel"
[PROOF STATE]
proof (state)
this:
(b, a) \<in> Rel
(b, c) \<in> Rel
(a, c) \<notin> Rel

goal (1 subgoal):
 1. (b, a) \<in> Rel \<and> (b, c) \<in> Rel \<and> (a, c) \<notin> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
with condB
[PROOF STATE]
proof (chain)
picking this:
\<forall>a b c. (a, b) \<in> Rel \<and> (a, c) \<in> Rel \<and> (b, c) \<notin> Rel \<longrightarrow> (b, a) \<in> Rel \<or> (c, a) \<in> Rel
(b, a) \<in> Rel
(b, c) \<in> Rel
(a, c) \<notin> Rel
[PROOF STEP]
have "(a, b) \<in> Rel \<or> (c, b) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<forall>a b c. (a, b) \<in> Rel \<and> (a, c) \<in> Rel \<and> (b, c) \<notin> Rel \<longrightarrow> (b, a) \<in> Rel \<or> (c, a) \<in> Rel
(b, a) \<in> Rel
(b, c) \<in> Rel
(a, c) \<notin> Rel

goal (1 subgoal):
 1. (a, b) \<in> Rel \<or> (c, b) \<in> Rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(a, b) \<in> Rel \<or> (c, b) \<in> Rel

goal (1 subgoal):
 1. (b, a) \<in> Rel \<and> (b, c) \<in> Rel \<and> (a, c) \<notin> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
thus "(a, c) \<in> symcl Rel"
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> Rel \<or> (c, b) \<in> Rel

goal (1 subgoal):
 1. (a, c) \<in> symcl Rel
[PROOF STEP]
proof auto
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (a, b) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
 2. (c, b) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
assume "(a, b) \<in> Rel"
[PROOF STATE]
proof (state)
this:
(a, b) \<in> Rel

goal (2 subgoals):
 1. (a, b) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
 2. (c, b) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
with B2 tranR
[PROOF STATE]
proof (chain)
picking this:
(b, c) \<in> Rel
trans Rel
(a, b) \<in> Rel
[PROOF STEP]
have "(a, c) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(b, c) \<in> Rel
trans Rel
(a, b) \<in> Rel

goal (1 subgoal):
 1. (a, c) \<in> Rel
[PROOF STEP]
unfolding trans_def
[PROOF STATE]
proof (prove)
using this:
(b, c) \<in> Rel
\<forall>x y z. (x, y) \<in> Rel \<longrightarrow> (y, z) \<in> Rel \<longrightarrow> (x, z) \<in> Rel
(a, b) \<in> Rel

goal (1 subgoal):
 1. (a, c) \<in> Rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(a, c) \<in> Rel

goal (2 subgoals):
 1. (a, b) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
 2. (c, b) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
thus "(a, c) \<in> symcl Rel"
[PROOF STATE]
proof (prove)
using this:
(a, c) \<in> Rel

goal (1 subgoal):
 1. (a, c) \<in> symcl Rel
[PROOF STEP]
by (simp add: symcl_def)
[PROOF STATE]
proof (state)
this:
(a, c) \<in> symcl Rel

goal (1 subgoal):
 1. (c, b) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (c, b) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
assume "(c, b) \<in> Rel"
[PROOF STATE]
proof (state)
this:
(c, b) \<in> Rel

goal (1 subgoal):
 1. (c, b) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
with B1 tranR
[PROOF STATE]
proof (chain)
picking this:
(b, a) \<in> Rel
trans Rel
(c, b) \<in> Rel
[PROOF STEP]
have "(c, a) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(b, a) \<in> Rel
trans Rel
(c, b) \<in> Rel

goal (1 subgoal):
 1. (c, a) \<in> Rel
[PROOF STEP]
unfolding trans_def
[PROOF STATE]
proof (prove)
using this:
(b, a) \<in> Rel
\<forall>x y z. (x, y) \<in> Rel \<longrightarrow> (y, z) \<in> Rel \<longrightarrow> (x, z) \<in> Rel
(c, b) \<in> Rel

goal (1 subgoal):
 1. (c, a) \<in> Rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(c, a) \<in> Rel

goal (1 subgoal):
 1. (c, b) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
thus "(a, c) \<in> symcl Rel"
[PROOF STATE]
proof (prove)
using this:
(c, a) \<in> Rel

goal (1 subgoal):
 1. (a, c) \<in> symcl Rel
[PROOF STEP]
by (simp add: symcl_def)
[PROOF STATE]
proof (state)
this:
(a, c) \<in> symcl Rel

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(a, c) \<in> symcl Rel

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(b, a) \<in> Rel \<and> (b, c) \<in> Rel \<and> (a, c) \<notin> Rel \<Longrightarrow> (a, c) \<in> symcl Rel

goal (1 subgoal):
 1. \<And>x y z. (x, y) \<in> symcl Rel \<and> (y, z) \<in> symcl Rel \<Longrightarrow> (x, z) \<in> symcl Rel
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(b, a) \<in> Rel \<and> (b, c) \<in> Rel \<and> (a, c) \<notin> Rel \<Longrightarrow> (a, c) \<in> symcl Rel

goal (1 subgoal):
 1. \<And>x y z. (x, y) \<in> symcl Rel \<and> (y, z) \<in> symcl Rel \<Longrightarrow> (x, z) \<in> symcl Rel
[PROOF STEP]
have "\<lbrakk>(b, a) \<in> Rel; (c, b) \<in> Rel\<rbrakk> \<Longrightarrow> (a, c) \<in> symcl Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b, a) \<in> Rel \<and> (c, b) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (b, a) \<in> Rel \<and> (c, b) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
assume "(c, b) \<in> Rel" and "(b, a) \<in> Rel"
[PROOF STATE]
proof (state)
this:
(c, b) \<in> Rel
(b, a) \<in> Rel

goal (1 subgoal):
 1. (b, a) \<in> Rel \<and> (c, b) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
with tranR
[PROOF STATE]
proof (chain)
picking this:
trans Rel
(c, b) \<in> Rel
(b, a) \<in> Rel
[PROOF STEP]
have "(c, a) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
trans Rel
(c, b) \<in> Rel
(b, a) \<in> Rel

goal (1 subgoal):
 1. (c, a) \<in> Rel
[PROOF STEP]
unfolding trans_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x y z. (x, y) \<in> Rel \<longrightarrow> (y, z) \<in> Rel \<longrightarrow> (x, z) \<in> Rel
(c, b) \<in> Rel
(b, a) \<in> Rel

goal (1 subgoal):
 1. (c, a) \<in> Rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(c, a) \<in> Rel

goal (1 subgoal):
 1. (b, a) \<in> Rel \<and> (c, b) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
thus "(a, c) \<in> symcl Rel"
[PROOF STATE]
proof (prove)
using this:
(c, a) \<in> Rel

goal (1 subgoal):
 1. (a, c) \<in> symcl Rel
[PROOF STEP]
by (simp add: symcl_def)
[PROOF STATE]
proof (state)
this:
(a, c) \<in> symcl Rel

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(b, a) \<in> Rel \<and> (c, b) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel

goal (1 subgoal):
 1. \<And>x y z. (x, y) \<in> symcl Rel \<and> (y, z) \<in> symcl Rel \<Longrightarrow> (x, z) \<in> symcl Rel
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(b, a) \<in> Rel \<and> (c, b) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel

goal (1 subgoal):
 1. \<And>x y z. (x, y) \<in> symcl Rel \<and> (y, z) \<in> symcl Rel \<Longrightarrow> (x, z) \<in> symcl Rel
[PROOF STEP]
assume "(a, b) \<in> symcl Rel" and "(b, c) \<in> symcl Rel"
[PROOF STATE]
proof (state)
this:
(a, b) \<in> symcl Rel
(b, c) \<in> symcl Rel

goal (1 subgoal):
 1. \<And>x y z. (x, y) \<in> symcl Rel \<and> (y, z) \<in> symcl Rel \<Longrightarrow> (x, z) \<in> symcl Rel
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(a, b) \<in> Rel \<and> (b, c) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
(a, b) \<in> Rel \<and> (c, b) \<in> Rel \<and> (a, c) \<notin> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
(b, a) \<in> Rel \<and> (b, c) \<in> Rel \<and> (a, c) \<notin> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
(b, a) \<in> Rel \<and> (c, b) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
(a, b) \<in> symcl Rel
(b, c) \<in> symcl Rel
[PROOF STEP]
show "(a, c) \<in> symcl Rel"
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> Rel \<and> (b, c) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
(a, b) \<in> Rel \<and> (c, b) \<in> Rel \<and> (a, c) \<notin> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
(b, a) \<in> Rel \<and> (b, c) \<in> Rel \<and> (a, c) \<notin> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
(b, a) \<in> Rel \<and> (c, b) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
(a, b) \<in> symcl Rel
(b, c) \<in> symcl Rel

goal (1 subgoal):
 1. (a, c) \<in> symcl Rel
[PROOF STEP]
by (auto simp add: symcl_def)
[PROOF STATE]
proof (state)
this:
(a, c) \<in> symcl Rel

goal:
No subgoals!
[PROOF STEP]
qed