let G be _Graph; :: thesis: ( G is _trivial iff the_Vertices_of G is trivial )
thus ( G is _trivial implies the_Vertices_of G is trivial ) ; :: thesis: ( the_Vertices_of G is trivial implies G is _trivial )
assume A1: the_Vertices_of G is trivial ; :: thesis: G is _trivial
assume not G is _trivial ; :: thesis: contradiction
then consider v1, v2 being Vertex of G such that
A2: v1 <> v2 by GLIB_000:21;
thus contradiction by A1, A2, ZFMISC_1:def 10; :: thesis: verum