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

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