let G be _Graph; :: thesis:

hereby :: thesis:

assume A1: not G is _trivial ; :: thesis:
set v1 = the Vertex of G;
set v2 = the Vertex of G;
reconsider H = the removeVertex of G, the Vertex of G as Subgraph of G ;
take H = H; :: thesis:
A2: the_Vertices_of H = (the_Vertices_of G) \ { the Vertex of G} by A1, GLIB_000:47;
the Vertex of G in { the Vertex of G} by TARSKI:def 1;
then the_Vertices_of H <> the_Vertices_of G by A2, XBOOLE_0:def 5;
hence not H is spanning by GLIB_000:def 33; :: thesis:

end;

given H being Subgraph of G such that A3: not H is spanning ; :: thesis:
A4: the_Vertices_of G <> the_Vertices_of H by A3, GLIB_000:def 33;
the_Vertices_of H c= the_Vertices_of G ;
then reconsider v1 = the Vertex of H as Vertex of G by TARSKI:def 3;
not the_Vertices_of G c= the_Vertices_of H by A4, XBOOLE_0:def 10;
then A5: (the_Vertices_of G) \ (the_Vertices_of H) <> {} by XBOOLE_1:37;
set v2 = the Element of (the_Vertices_of G) \ (the_Vertices_of H);
reconsider v2 = the Element of (the_Vertices_of G) \ (the_Vertices_of H) as Vertex of G by A5, TARSKI:def 3;
A6: v1 <> v2 by A5, XBOOLE_0:def 5;
card {v1,v2} c= card (the_Vertices_of G) by CARD_1:11;
then A7: 2 c= card (the_Vertices_of G) by A6, CARD_2:57;
assume G is _trivial ; :: thesis:
then A8: 2 c= 1 by A7, GLIB_000:def 19;
1 in {0,1} by TARSKI:def 2;
then 1 in 1 by A8, CARD_1:50;
hence contradiction ; :: thesis: