Theorem: FilterGame.Basis.mem_as_filter_of_mem (FilterGame/Basis.lean)

State before:
α : Type u_1
b : Basis α
s : Set α
h : s ∈ b
⊢ s ∈ as_filter b
Tactic:
sorry
State after:
no goals