let G be _Graph; :: thesis: ( G is trivial implies G is complete )

assume G is trivial ; :: thesis: G is complete

then consider x being Vertex of G such that

A1: the_Vertices_of G = {x} by GLIB_000:22;

let u, v be Vertex of G; :: according to CHORD:def 6 :: thesis: ( u <> v implies u,v are_adjacent )

assume that

A2: u <> v and

not u,v are_adjacent ; :: thesis: contradiction

u = x by A1, TARSKI:def 1;

hence contradiction by A1, A2, TARSKI:def 1; :: thesis: verum

assume G is trivial ; :: thesis: G is complete

then consider x being Vertex of G such that

A1: the_Vertices_of G = {x} by GLIB_000:22;

let u, v be Vertex of G; :: according to CHORD:def 6 :: thesis: ( u <> v implies u,v are_adjacent )

assume that

A2: u <> v and

not u,v are_adjacent ; :: thesis: contradiction

u = x by A1, TARSKI:def 1;

hence contradiction by A1, A2, TARSKI:def 1; :: thesis: verum