Theorem cusgrusgr

Description: A complete simple graph is a simple graph. (Contributed by Alexander van der Vekens, 13-Oct-2017) (Revised by AV, 1-Nov-2020)

	Ref	Expression
Assertion	cusgrusgr	⊢ ( 𝐺 ∈ ComplUSGraph → 𝐺 ∈ USGraph )

Proof

Step	Hyp	Ref	Expression
1		iscusgr	⊢ ( 𝐺 ∈ ComplUSGraph ↔ ( 𝐺 ∈ USGraph ∧ 𝐺 ∈ ComplGraph ) )
2	1	simplbi	⊢ ( 𝐺 ∈ ComplUSGraph → 𝐺 ∈ USGraph )