proposition: Lemma clusterE F : cluster F = \bigcap_(A in F) (closure A).
proof: Proof. by rewrite predeqE => p; split=> cF ????; apply: cF. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed