Definition df-cusgr

Description: Define the class of all complete simple graphs. A simple graph is called complete if every pair of distinct vertices is connected by a (unique) edge, see definition in section 1.1 of Diestel p. 3. In contrast, the definition in section I.1 of Bollobas p. 3 is based on the size of (finite) complete graphs, see cusgrsize . (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 24-Oct-2020) (Revised by BJ, 14-Feb-2022)

	Ref	Expression
Assertion	df-cusgr	|- ComplUSGraph = ( USGraph i^i ComplGraph )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccusgr	|- ComplUSGraph
1		cusgr	|- USGraph
2		ccplgr	|- ComplGraph
3	1 2	cin	|- ( USGraph i^i ComplGraph )
4	0 3	wceq	|- ComplUSGraph = ( USGraph i^i ComplGraph )