α : Type u_1
S s : Set α
h_s : s ∈ {S}
t : Set α
h_t : t ∈ {S}
a✝ : Set.Nonempty (s ∩ t)
⊢ s ∩ t ∈ {S}
α : Type u_1
S : Set α
⊢ IsPiSystem {S}
intro s h_s t h_t _
no goals
α : Type u_1
S s : Set α
h_s : s ∈ {S}
t : Set α
h_t : t ∈ {S}
a✝ : Set.Nonempty (s ∩ t)
⊢ s ∩ t ∈ {S}
rw [Set.mem_singleton_iff.1 h_s, Set.mem_singleton_iff.1 h_t, Set.inter_self,
  Set.mem_singleton_iff]