Metamath Proof Explorer

Theorem umgruhgr

Description: An undirected multigraph is an undirected hypergraph. (Contributed by AV, 26-Nov-2020)

		Ref	Expression
	Assertion	umgruhgr	$⊢ G \in UMGraph \to G \in UHGraph$

Step	Hyp	Ref	Expression
1		umgrupgr	$⊢ G \in UMGraph \to G \in UPGraph$
2		upgruhgr	$⊢ G \in UPGraph \to G \in UHGraph$
3	1 2	syl	$⊢ G \in UMGraph \to G \in UHGraph$