Metamath Proof Explorer


Theorem cusgr0

Description: The null graph (with no vertices and no edges) represented by the empty set is a complete simple graph. (Contributed by AV, 1-Nov-2020)

Ref Expression
Assertion cusgr0 ∅ ∈ ComplUSGraph

Proof

Step Hyp Ref Expression
1 usgr0 ∅ ∈ USGraph
2 cplgr0 ∅ ∈ ComplGraph
3 iscusgr ( ∅ ∈ ComplUSGraph ↔ ( ∅ ∈ USGraph ∧ ∅ ∈ ComplGraph ) )
4 1 2 3 mpbir2an ∅ ∈ ComplUSGraph