proposition: Lemma saturated2P r x: equivalence r -> sub x (substrate r) -> ((saturated r x) <-> exists2 y, (forall z, inc z y -> classp r z) & x = union y).
proof: Proof. move => er sxs; move: (saturatedP er sxs) => aux;split. move => srx. exists (Zo (\Po x)(fun z => exists2 a, inc a x & z = class r a)). move=> z /Zo_P [] /setP_P zx [a ax ->]. by apply: class_class =>//; apply: sxs. set_extens t => ts. apply: (@setU_i _ (class r t)). by move: (sxs _ ts)=>h; apply/(class_P er);equiv_tac. apply: Zo_i; [ by apply/setP_P;move /aux: srx; apply | ex_tac]. by move /setU_P: ts => [y ty /Zo_P [] /setP_P yx [a ax yc]]; apply: yx. move => [y yp xu]; apply/aux; rewrite xu => z zu. move: (setU_hi zu) =>[t zt ty]; move: (yp _ ty) => ct. move => u /(class_P er) rz; apply:(setU_i _ ty). have pa := (rel_in_class er ct zt). rewrite (proj2 (yp _ ty)); apply /(class_P er); equiv_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)