[STATEMENT]
theorem Theorem_3:
  assumes "\<forall>h. irc_on A (Ch h)"
  shows "(\<forall>h. substitutes_on A (Ch h)) \<longleftrightarrow> (\<forall>h. unilateral_substitutes_on A (Ch h) \<and> pareto_separable_on A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>h. substitutes_on A (Ch h)) = (\<forall>h. unilateral_substitutes_on A (Ch h) \<and> pareto_separable_on A)
[PROOF STEP]
using %invisible assms
      unilateral_substitutes_on_pareto_separable_on_substitutes_on substitutes_on_pareto_separable_on
      substitutes_on_unilateral_substitutes_on
[PROOF STATE]
proof (prove)
using this:
\<forall>h. irc_on A (Ch h)
\<lbrakk>\<forall>h. unilateral_substitutes_on ?A (Ch h); \<forall>h. irc_on ?A (Ch h); pareto_separable_on ?A\<rbrakk> \<Longrightarrow> substitutes_on ?A (Ch ?h)
\<forall>h. substitutes_on ?A (Ch h) \<Longrightarrow> pareto_separable_on ?A
substitutes_on ?A ?f \<Longrightarrow> unilateral_substitutes_on ?A ?f

goal (1 subgoal):
 1. (\<forall>h. substitutes_on A (Ch h)) = (\<forall>h. unilateral_substitutes_on A (Ch h) \<and> pareto_separable_on A)
[PROOF STEP]
by blast