proposition: Lemma small_set_sub (E : set Y) : F E -> \forall E' \near powerset_filter_from, E' `<=` E.
proof: Proof. move=> entE; exists [set E' | F E' /\ E' `<=` E]; last by move=> ? []. split; [by move=> E' [] | | by exists E; split]. by move=> E1 E2 [] ? subE ? ?; split => //; exact: subset_trans subE. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed