chore(order/filter/bases): golf a proof (#4834)
* rename `filter.has_basis.forall_nonempty_iff_ne_bot` to
`filter.has_basis.ne_bot_iff`, swap LHS with RHS;
* add `filter.has_basis.eq_bot_iff`;
* golf the proof of `filter.has_basis.ne_bot` using `filter.has_basis.forall_iff`.
