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