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