set v = the Vertex of G;
set H = the inducedSubgraph of G,{ the Vertex of G};
the_Vertices_of the inducedSubgraph of G,{ the Vertex of G} <> the_Vertices_of G

proof

assume A1: the_Vertices_of the inducedSubgraph of G,{ the Vertex of G} = the_Vertices_of G ; :: thesis: contradiction
1 = card (the_Vertices_of G) by A1, GLIB_000:def 19;
hence contradiction by GLIB_000:def 19; :: thesis: verum

end;

hence ex b₁ being Subgraph of G st
( not b₁ is spanning & b₁ is _trivial & b₁ is connected ) by GLIB_000:def 33; :: thesis: verum