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

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