no goals
ι : Sort ?u.104778
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
H₁ H₂ : Subgraph G
⊢ ∀ (x y : V),
    Quotient.mk (Sym2.Rel.setoid V) (x, y) ∈ edgeSet (H₁ ⊓ H₂) ↔
      Quotient.mk (Sym2.Rel.setoid V) (x, y) ∈ edgeSet H₁ ∩ edgeSet H₂
simp