proposition: Lemma pure_properties_res6 A S: pure_prop1 A S -> pure_prop2 S -> pure_prop3 A S -> pure_prop4 S -> exists R, [/\ mobile_ext R A, S = (set_of_pure A R) & (forall x z, inc x R -> inc z R -> sub x z -> z = x)].
proof: Proof. move => p1 p2 p3 p4; apply: pure_properties_res5 => //. by apply: pure_properties_res4. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)