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