[STATEMENT]
lemma surj_Sup_pres_inj:
  fixes f :: "'a::complete_lattice_with_dual \<Rightarrow> 'b::complete_lattice_with_dual"
  assumes "surj f"
  and "Sup_pres f" 
  shows "inj (radj f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj (radj f)
[PROOF STEP]
by (metis assms comp_eq_dest_lhs id_apply injI surj_Sup_pres_id)