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 b1 being Subgraph of G st
( not b1 is spanning & b1 is _trivial & b1 is connected ) by GLIB_000:def 33; :: thesis: verum