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