Theorem cusgrcplgr

Description: A complete simple graph is a complete graph. (Contributed by AV, 1-Nov-2020)

	Ref	Expression
Assertion	cusgrcplgr	⊢ ( 𝐺 ∈ ComplUSGraph → 𝐺 ∈ ComplGraph )

Proof

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