let G be _Graph; :: thesis: ( not G is _trivial iff ex H being Subgraph of G st not H is spanning )

hereby :: thesis: ( not for H being Subgraph of G holds H is spanning implies not G is _trivial )

assume A1: not G is _trivial ; :: thesis: not for H being Subgraph of G holds H is spanning
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: not H is spanning
A2: the_Vertices_of H = (the_Vertices_of G) \ { the Vertex of G} by A1, Th47;
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 ; :: thesis: verum

end;

given H being Subgraph of G such that A3: not H is spanning ; :: thesis: not G is _trivial
A4: the_Vertices_of G <> the_Vertices_of H by A3;
the_Vertices_of H c= the_Vertices_of G ;
then reconsider v1 = the Vertex of H as Vertex of G ;
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: contradiction
then A8: 2 c= 1 by A7;
1 in {0,1} by TARSKI:def 2;
then 1 in 1 by A8, CARD_1:50;
hence contradiction ; :: thesis: verum