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:25;
let u, v be Vertex of G; :: according to CHORD:def 6 :: thesis: ( u <> v implies u,v are_adjacent )
assume A2: ( u <> v & not u,v are_adjacent ) ; :: thesis: contradiction
( u = x & v = x ) by A1, TARSKI:def 1;
hence contradiction by A2; :: thesis: verum