intro hxs y hfxy
α : Type u_1
s t u : Set α
β : Type u_1
f : α → Set β
x : α
⊢ x ∈ s → (f x).Subset (s >>= f)
α : Type u_1
s t u : Set α
β : Type u_1
f : α → Set β
x : α
hxs : x ∈ s
y : β
hfxy : y ∈ f x
⊢ y ∈ s >>= f