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