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	|- (/) e. ComplUSGraph

Proof

Step	Hyp	Ref	Expression
1		usgr0	|- (/) e. USGraph
2		cplgr0	|- (/) e. ComplGraph
3		iscusgr	|- ( (/) e. ComplUSGraph <-> ( (/) e. USGraph /\ (/) e. ComplGraph ) )
4	1 2 3	mpbir2an	|- (/) e. ComplUSGraph