Metamath Proof Explorer

Theorem umgruhgr

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

Ref Expression
Assertion umgruhgr 
|- ( G e. UMGraph -> G e. UHGraph )

Proof

Step Hyp Ref Expression
1 umgrupgr 
 |-  ( G e. UMGraph -> G e. UPGraph )
2 upgruhgr 
 |-  ( G e. UPGraph -> G e. UHGraph )
3 1 2 syl 
 |-  ( G e. UMGraph -> G e. UHGraph )