[STATEMENT]
lemma connected_Ioo[simp]: "connected {a<..<b}"
  for a b :: "'a::linear_continuum_topology"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. connected {a<..<b}
[PROOF STEP]
unfolding connected_iff_interval
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{a<..<b}. \<forall>y\<in>{a<..<b}. \<forall>z\<ge>x. z \<le> y \<longrightarrow> z \<in> {a<..<b}
[PROOF STEP]
by auto