defpred S1[ Nat] means for G being _finite connected _Graph st (G .order()) + $1 = (G .size()) + 1 holds
ex H being Subgraph of G st
( H is spanning & H is Tree-like & H is connected & H is acyclic );
A1: S1[ 0 ]
proof
let G be _finite connected _Graph; :: thesis: ( (G .order()) + 0 = (G .size()) + 1 implies ex H being Subgraph of G st
( H is spanning & H is Tree-like & H is connected & H is acyclic ) )
assume A2: (G .order()) + 0 = (G .size()) + 1 ; :: thesis: ex H being Subgraph of G st
( H is spanning & H is Tree-like & H is connected & H is acyclic )
reconsider H = G as Subgraph of G by GLIB_000:40;
take H ; :: thesis: ( H is spanning & H is Tree-like & H is connected & H is acyclic )
the_Vertices_of H = the_Vertices_of G ;
hence H is spanning by GLIB_000:def 33; :: thesis: ( H is Tree-like & H is connected & H is acyclic )
thus H is Tree-like by A2, GLIB_002:47; :: thesis: ( H is connected & H is acyclic )
hence ( H is connected & H is acyclic ) ; :: thesis: verum
end;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; :: thesis: S1[k + 1]
let G be _finite connected _Graph; :: thesis: ( (G .order()) + (k + 1) = (G .size()) + 1 implies ex H being Subgraph of G st
( H is spanning & H is Tree-like & H is connected & H is acyclic ) )
assume A5: (G .order()) + (k + 1) = (G .size()) + 1 ; :: thesis: ex H being Subgraph of G st
( H is spanning & H is Tree-like & H is connected & H is acyclic )
k + 1 <> 0 ;
then G .order() <> (G .size()) + 1 by A5;
then not G is acyclic by GLIB_002:47;
then consider C being Walk of G such that
A6: C is Cycle-like by GLIB_002:def 2;
A7: not C .edges() is empty by A6, GLIB_001:136;
set e = the Element of C .edges() ;
set G2 = the removeEdge of G, the Element of C .edges() ;
A8: the removeEdge of G, the Element of C .edges() is connected by A6, A7, GLIB_002:5;
((G .order()) + k) + 1 = (( the removeEdge of G, the Element of C .edges() .size()) + 1) + 1 by A5, A7, TARSKI:def 3, GLIB_000:52;
then ( the removeEdge of G, the Element of C .edges() .order()) + k = ( the removeEdge of G, the Element of C .edges() .size()) + 1 by GLIB_000:52;
then consider H being Subgraph of the removeEdge of G, the Element of C .edges() such that
A9: ( H is spanning & H is Tree-like & H is connected & H is acyclic ) by A4, A8;
reconsider H = H as spanning Subgraph of G by A9, GLIB_000:74;
take H ; :: thesis: ( H is spanning & H is Tree-like & H is connected & H is acyclic )
thus ( H is spanning & H is Tree-like & H is connected & H is acyclic ) by A9; :: thesis: verum
end;
A10: for k being Nat holds S1[k] from NAT_1:sch 2(A1, A3);
 let G be _finite connected _Graph; :: thesis: ex H being Subgraph of G st
( H is spanning & H is Tree-like & H is connected & H is acyclic )
ex k being Nat st (G .size()) + 1 = (G .order()) + k by GLIB_002:40, NAT_1:10;
hence ex H being Subgraph of G st
( H is spanning & H is Tree-like & H is connected & H is acyclic ) by A10; :: thesis: verum