[STATEMENT]
lemma open_segment_Reals:
    "\<lbrakk>x \<in> Reals; y \<in> Reals\<rbrakk> \<Longrightarrow> open_segment x y = of_real ` open_segment (Re x) (Re y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> \<real>; y \<in> \<real>\<rbrakk> \<Longrightarrow> open_segment x y = complex_of_real ` open_segment (Re x) (Re y)
[PROOF STEP]
by (metis open_segment_of_real of_real_Re)