defpred S1[ Nat] means for G being _finite acyclic _Graph st G .order() = $1 & G .order() = (G .size()) + 1 holds
G is connected ;
let G be _finite _Graph; :: thesis: ( G is Tree-like iff ( G is acyclic & G .order() = (G .size()) + 1 ) )
hereby :: thesis: ( G is acyclic & G .order() = (G .size()) + 1 implies G is Tree-like )
defpred S2[ Nat] means for T being _finite Tree-like _Graph st T .order() = $1 holds
$1 = (T .size()) + 1;
assume A1: G is Tree-like ; :: thesis: ( G is acyclic & G .order() = (G .size()) + 1 )
hence G is acyclic ; :: thesis: G .order() = (G .size()) + 1
now :: thesis: for T being _finite Tree-like _Graph st T .order() = 1 holds
1 = (T .size()) + 1
let T be _finite Tree-like _Graph; :: thesis: ( T .order() = 1 implies 1 = (T .size()) + 1 )
set VT = the_Vertices_of T;
set ET = the_Edges_of T;
assume T .order() = 1 ; :: thesis: 1 = (T .size()) + 1
then card (the_Vertices_of T) = 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 A2, TARSKI:def 1;
then card (the_Edges_of T) = 0 by CARD_1:27, XBOOLE_0:def 1;
then T .size() = 0 by GLIB_000:def 25;
hence 1 = (T .size()) + 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 = (T .size()) + 1 ) holds
for T being _finite Tree-like _Graph st T .order() = k + 1 holds
k + 1 = (T .size()) + 1
let k be non zero Nat; :: thesis: ( ( for T being _finite Tree-like _Graph st T .order() = k holds
k = (T .size()) + 1 ) implies for T being _finite Tree-like _Graph st T .order() = k + 1 holds
k + 1 = (T .size()) + 1 )
assume A6: for T being _finite Tree-like _Graph st T .order() = k holds
k = (T .size()) + 1 ; :: thesis: for T being _finite Tree-like _Graph st T .order() = k + 1 holds
k + 1 = (T .size()) + 1
let T be _finite Tree-like _Graph; :: thesis: ( T .order() = k + 1 implies k + 1 = (T .size()) + 1 )
assume A7: T .order() = k + 1 ; :: thesis: k + 1 = (T .size()) + 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 A7, GLIB_000:48;
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 = (T .size()) + 1 by A8, GLIB_000:48; :: 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() = (G .size()) + 1 by A1; :: thesis: verum
end;
assume that
A10: G is acyclic and
A11: G .order() = (G .size()) + 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() = (G .size()) + 1 holds
G is connected ) holds
for G being _finite acyclic _Graph st G .order() = k + 1 & G .order() = (G .size()) + 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() = (G .size()) + 1 holds
G is connected ) implies for G being _finite acyclic _Graph st G .order() = k + 1 & G .order() = (G .size()) + 1 holds
G is connected )
assume A12: for G being _finite acyclic _Graph st G .order() = k & G .order() = (G .size()) + 1 holds
G is connected ; :: thesis: for G being _finite acyclic _Graph st G .order() = k + 1 & G .order() = (G .size()) + 1 holds
G is connected
let G be _finite acyclic _Graph; :: thesis: ( G .order() = k + 1 & G .order() = (G .size()) + 1 implies G is connected )
assume that
A13: G .order() = k + 1 and
A14: G .order() = (G .size()) + 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 A13, A14, CARD_1:27, GLIB_000:def 25;
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()) + (card (v .edgesInOut())) = aG .size() ) by GLIB_000:48;
card (v .edgesInOut()) = v .degree() by GLIB_000:19
.= 1 by A15, GLIB_000:def 52 ;
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 A15, GLIB_000:def 51;
e in v .edgesInOut() by A18, TARSKI:def 1;
hence G is connected by A17, A19, Th2; :: 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() = (G .size()) + 1 holds
G is connected
let G be _finite acyclic _Graph; :: thesis: ( G .order() = 1 & G .order() = (G .size()) + 1 implies G is connected )
assume that
A21: G .order() = 1 and
G .order() = (G .size()) + 1 ; :: thesis: G is connected
consider v being Vertex of G such that
A22: the_Vertices_of G = {v} by A21, GLIB_000:27;
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 A22, TARSKI:def 1;
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 NAT_1:sch 10(A23, A20);
 then G is connected by A10, A11;
hence G is Tree-like by A10; :: thesis: verum