defpred S1[ Nat] means for G being finite acyclic _Graph st G .order() = \$1 & G .order() = () + 1 holds
G is connected ;
let G be finite _Graph; :: thesis: ( G is Tree-like iff ( G is acyclic & G .order() = () + 1 ) )
hereby :: thesis: ( G is acyclic & G .order() = () + 1 implies G is Tree-like )
defpred S2[ Nat] means for T being finite Tree-like _Graph st T .order() = \$1 holds
\$1 = () + 1;
assume A1: G is Tree-like ; :: thesis: ( G is acyclic & G .order() = () + 1 )
hence G is acyclic ; :: thesis: G .order() = () + 1
now :: thesis: for T being finite Tree-like _Graph st T .order() = 1 holds
1 = () + 1
let T be finite Tree-like _Graph; :: thesis: ( T .order() = 1 implies 1 = () + 1 )
set VT = the_Vertices_of T;
set ET = the_Edges_of T;
assume T .order() = 1 ; :: thesis: 1 = () + 1
then card () = 1 by GLIB_000:def 24;
then consider v being object such that
A2: the_Vertices_of T = {v} by CARD_2:42;
reconsider v = v as Vertex of T by ;
then card () = 0 by ;
then T .size() = 0 by GLIB_000:def 25;
hence 1 = () + 1 ; :: thesis: verum
end;
then A5: S2[1] ;
now :: thesis: for k being non zero Nat st ( for T being finite Tree-like _Graph st T .order() = k holds
k = () + 1 ) holds
for T being finite Tree-like _Graph st T .order() = k + 1 holds
k + 1 = () + 1
let k be non zero Nat; :: thesis: ( ( for T being finite Tree-like _Graph st T .order() = k holds
k = () + 1 ) implies for T being finite Tree-like _Graph st T .order() = k + 1 holds
k + 1 = () + 1 )

assume A6: for T being finite Tree-like _Graph st T .order() = k holds
k = () + 1 ; :: thesis: for T being finite Tree-like _Graph st T .order() = k + 1 holds
k + 1 = () + 1

let T be finite Tree-like _Graph; :: thesis: ( T .order() = k + 1 implies k + 1 = () + 1 )
assume A7: T .order() = k + 1 ; :: thesis: k + 1 = () + 1
then T .order() <> 1 by XCMPLX_1:3;
then reconsider aT = T as finite non trivial Tree-like _Graph by GLIB_000:26;
set v = the endvertex Vertex of aT;
set T2 = the removeVertex of aT, the endvertex Vertex of aT;
(( the removeVertex of aT, the endvertex Vertex of aT .order()) + 1) - 1 = (k + 1) - 1 by ;
then A8: k = ( the removeVertex of aT, the endvertex Vertex of aT .size()) + 1 by A6;
card ( the endvertex Vertex of aT .edgesInOut()) = the endvertex Vertex of aT .degree() by GLIB_000:19
.= 1 by GLIB_000:def 52 ;
hence k + 1 = () + 1 by ; :: thesis: verum
end;
then A9: for k being non zero Nat st S2[k] holds
S2[k + 1] ;
for k being non zero Nat holds S2[k] from NAT_1:sch 10(A5, A9);
hence G .order() = () + 1 by A1; :: thesis: verum
end;
assume that
A10: G is acyclic and
A11: G .order() = () + 1 ; :: thesis: G is Tree-like
now :: thesis: for k being non zero Element of NAT st ( for G being finite acyclic _Graph st G .order() = k & G .order() = () + 1 holds
G is connected ) holds
for G being finite acyclic _Graph st G .order() = k + 1 & G .order() = () + 1 holds
G is connected
let k be non zero Element of NAT ; :: thesis: ( ( for G being finite acyclic _Graph st G .order() = k & G .order() = () + 1 holds
G is connected ) implies for G being finite acyclic _Graph st G .order() = k + 1 & G .order() = () + 1 holds
G is connected )

assume A12: for G being finite acyclic _Graph st G .order() = k & G .order() = () + 1 holds
G is connected ; :: thesis: for G being finite acyclic _Graph st G .order() = k + 1 & G .order() = () + 1 holds
G is connected

let G be finite acyclic _Graph; :: thesis: ( G .order() = k + 1 & G .order() = () + 1 implies G is connected )
assume that
A13: G .order() = k + 1 and
A14: G .order() = () + 1 ; :: thesis: G is connected
now :: thesis: not G .order() = 1
assume G .order() = 1 ; :: thesis: contradiction
then 0 + 1 = k + 1 by A13;
hence contradiction ; :: thesis: verum
end;
then reconsider aG = G as finite non trivial acyclic _Graph by GLIB_000:26;
the_Edges_of G <> {} by ;
then consider v, v2 being Vertex of aG such that
v <> v2 and
A15: v is endvertex and
v2 is endvertex and
v2 in aG .reachableFrom v by Lm23;
set G2 = the removeVertex of G,v;
A16: ( ( the removeVertex of G,v .order()) + 1 = aG .order() & ( the removeVertex of G,v .size()) + () = aG .size() ) by GLIB_000:48;
card () = v .degree() by GLIB_000:19
.= 1 by ;
then A17: the removeVertex of G,v is connected by A12, A13, A14, A16;
consider e being object such that
A18: v .edgesInOut() = {e} and
A19: not e Joins v,v,G by ;
e in v .edgesInOut() by ;
hence G is connected by ; :: thesis: verum
end;
then A20: for k being non zero Nat st S1[k] holds
S1[k + 1] ;
now :: thesis: for G being finite acyclic _Graph st G .order() = 1 & G .order() = () + 1 holds
G is connected
let G be finite acyclic _Graph; :: thesis: ( G .order() = 1 & G .order() = () + 1 implies G is connected )
assume that
A21: G .order() = 1 and
G .order() = () + 1 ; :: thesis: G is connected
consider v being Vertex of G such that
A22: the_Vertices_of G = {v} by ;
now :: thesis: for v1, v2 being Vertex of G ex W being Walk of G st W is_Walk_from v1,v2
let v1, v2 be Vertex of G; :: thesis: ex W being Walk of G st W is_Walk_from v1,v2
( v1 = v & v2 = v ) by ;
then G .walkOf v is_Walk_from v1,v2 by GLIB_001:13;
hence ex W being Walk of G st W is_Walk_from v1,v2 ; :: thesis: verum
end;
hence G is connected ; :: thesis: verum
end;
then A23: S1[1] ;
for k being non zero Nat holds S1[k] from then G is connected by ;
hence G is Tree-like by A10; :: thesis: verum