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