set IT = the _finite _trivial simple Subgraph of G;
take the _finite _trivial simple Subgraph of G ; :: thesis: ( the _finite _trivial simple Subgraph of G is _trivial & the _finite _trivial simple Subgraph of G is _finite & the _finite _trivial simple Subgraph of G is Tree-like )
thus ( the _finite _trivial simple Subgraph of G is _trivial & the _finite _trivial simple Subgraph of G is _finite & the _finite _trivial simple Subgraph of G is Tree-like ) ; :: thesis: verum