theorem Th15: :: GLIB_008:15

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