theorem :: GLIB_000:121

for G being _Graph holds
( not G is _trivial iff ex H being Subgraph of G st not H is spanning )