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	$$⊢\mathrm{ComplUSGraph}=\mathrm{USGraph}\cap \mathrm{ComplGraph}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccusgr	$$class\mathrm{ComplUSGraph}$$
1		cusgr	$$class\mathrm{USGraph}$$
2		ccplgr	$$class\mathrm{ComplGraph}$$
3	1 2	cin	$$class\left(\mathrm{USGraph}\cap \mathrm{ComplGraph}\right)$$
4	0 3	wceq	$$wff\mathrm{ComplUSGraph}=\mathrm{USGraph}\cap \mathrm{ComplGraph}$$