[STATEMENT]
lemma (in Order) ord_isom_surj_forall:"\<lbrakk>Order E; ord_isom D E f\<rbrakk> \<Longrightarrow>
              \<forall>b \<in> carrier E. \<exists>a\<in>carrier D. b = f a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Order E; ord_isom D E f\<rbrakk> \<Longrightarrow> \<forall>b\<in>carrier E. \<exists>a\<in>carrier D. b = f a
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>Order E; ord_isom D E f; b \<in> carrier E\<rbrakk> \<Longrightarrow> \<exists>a\<in>carrier D. b = f a
[PROOF STEP]
apply (rule ord_isom_surj[of "E" "f"], assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done