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 )

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
defpred S₁[ Nat] means for T being finite Tree-like _Graph st T .order() = $1 holds
$1 = (T .size() ) + 1;

now

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 26;
then consider v being set such that
A2: the_Vertices_of T = {v} by CARD_2:60;
reconsider v = v as Vertex of T by A2, TARSKI:def 1;

now

assume ex e being set st e in the_Edges_of T ; :: thesis: contradiction
then consider e being set such that
A3: e in the_Edges_of T ;
( (the_Source_of T) . e in {v} & (the_Target_of T) . e in {v} ) by A2, A3, FUNCT_2:7;
then ( (the_Source_of T) . e = v & (the_Target_of T) . e = v ) by TARSKI:def 1;
then e Joins v,v,T by A3, GLIB_000:def 15;
then T .walkOf v,e,v is Cycle-like by GLIB_001:157;
hence contradiction by Def2; :: thesis: verum

end;

then card (the_Edges_of T) = 0 by CARD_1:47, XBOOLE_0:def 1;
then T .size() = 0 by GLIB_000:def 27;
hence 1 = (T .size() ) + 1 ; :: thesis: verum

end;

then A4: S₁[1] ;

now

let k be non empty 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 A5: 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 A6: 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:29;
consider v being endvertex Vertex of aT;
consider T2 being removeVertex of aT,v;
((T2 .order() ) + 1) - 1 = (k + 1) - 1 by A6, GLIB_000:51;
then A7: k = (T2 .size() ) + 1 by A5;
card (v .edgesInOut() ) = v .degree() by GLIB_000:22
.= 1 by GLIB_000:def 54 ;
hence k + 1 = (T .size() ) + 1 by A7, GLIB_000:51; :: thesis: verum

end;

then A8: for k being non empty Nat st S₁[k] holds
S₁[k + 1] ;
for k being non empty Nat holds S₁[k] from NAT_1:sch 10(A4, A8);
hence G .order() = (G .size() ) + 1 by A1; :: thesis: verum

end;

assume A9: ( G is acyclic & G .order() = (G .size() ) + 1 ) ; :: thesis: G is Tree-like
defpred S₁[ Nat] means for G being finite acyclic _Graph st G .order() = $1 & G .order() = (G .size() ) + 1 holds
G is connected ;

now

let G be finite acyclic _Graph; :: thesis: ( G .order() = 1 & G .order() = (G .size() ) + 1 implies G is connected )
assume ( G .order() = 1 & G .order() = (G .size() ) + 1 ) ; :: thesis: G is connected
then consider v being Vertex of G such that
A10: the_Vertices_of G = {v} by GLIB_000:30;

now

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 A10, TARSKI:def 1;
then G .walkOf v is_Walk_from v1,v2 by GLIB_001:14;
hence ex W being Walk of G st W is_Walk_from v1,v2 ; :: thesis: verum

end;

hence G is connected by Def1; :: thesis: verum

end;

then A11: S₁[1] ;

now

let k be non empty 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 A13: ( G .order() = k + 1 & G .order() = (G .size() ) + 1 ) ; :: thesis: G is connected

now

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:29;
the_Edges_of G <> {} by A13, CARD_1:47, GLIB_000:def 27;
then consider v, v2 being Vertex of aG such that
A14: ( v <> v2 & v is endvertex & v2 is endvertex & v2 in aG .reachableFrom v ) by Lm23;
consider G2 being removeVertex of G,v;
A15: ( (G2 .order() ) + 1 = aG .order() & (G2 .size() ) + (card (v .edgesInOut() )) = aG .size() ) by GLIB_000:51;
card (v .edgesInOut() ) = v .degree() by GLIB_000:22
.= 1 by A14, GLIB_000:def 54 ;
then A16: G2 is connected by A12, A13, A15;
consider e being set such that
A17: ( v .edgesInOut() = {e} & not e Joins v,v,G ) by A14, GLIB_000:def 53;
e in v .edgesInOut() by A17, TARSKI:def 1;
hence G is connected by A16, A17, Th3; :: thesis: verum

end;

then A18: for k being non empty Nat st S₁[k] holds
S₁[k + 1] ;
for k being non empty Nat holds S₁[k] from NAT_1:sch 10(A11, A18);
then G is connected by A9;
hence G is Tree-like by A9; :: thesis: verum