let G2 be Subgraph of G; :: thesis: ( G2 is spanning implies not G2 is _trivial )
assume G2 is spanning ; :: thesis: not G2 is _trivial
then the_Vertices_of G2 = the_Vertices_of G by GLIB_000:def 33;
then card (the_Vertices_of G2) <> 1 by GLIB_000:def 19;
hence not G2 is _trivial by GLIB_000:def 19; :: thesis: verum