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 ]
A3:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A4:
S1[
k]
;
S1[k + 1]
let G be
_finite connected _Graph;
( (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
;
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
;
( 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;
verum
end;
A10:
for k being Nat holds S1[k]
from NAT_1:sch 2(A1, A3);
let G be _finite connected _Graph; 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; verum