proposition: Lemma ext2_pr5 E E' g z: bijection_prop g E E' -> inc z (\Po (\Po E)) -> inc (extension_p3 g z) (\Po (\Po E')).
proof: Proof. move => bg zz; apply/setP_P => t /(ext2_pr3 bg zz) [u uz ->]. move:(bg) => [[[fg _] _] _ <-]. apply/setP_P; apply:(fun_image_Starget1 fg). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)