[STATEMENT]
lemma connected_Iic[simp]: "connected {..a}"
  for a :: "'a::linear_continuum_topology"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. connected {..a}
[PROOF STEP]
by (auto simp: connected_iff_interval)