proposition: Lemma meetsxx T (F : set_system T) (FF : Filter F) : F `#` F = ~ (F set0).
proof: Proof. rewrite propeqE; split => [FmF F0|]; first by have [x []] := FmF _ _ F0 F0. move=> FN0 A B /filterI FAI {}/FAI FAB; apply/set0P/eqP => AB0. by rewrite AB0 in FAB. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed