Metamath Proof Explorer


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 )