proposition: Lemma image_affixe : forall M : PO, image (affixe M) = M.
proof: Proof. intros. elim existence_affixe_point with (M := M); intros z H; try clear existence_affixe_point; try exact H. rewrite <- H; symmetry in |- *; auto with geo. Qed.