defpred S₁[ 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 S₂[ 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

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_Target_of T) . e in {v} by A2, A3, FUNCT_2:7;
then A4: (the_Target_of T) . e = v by TARSKI:def 1;
(the_Source_of T) . e in {v} by A2, A3, FUNCT_2:7;
then (the_Source_of T) . e = v by TARSKI:def 1;
then e Joins v,v,T by A3, A4, 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 A5: 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 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:29;
consider v being endvertex Vertex of aT;
consider T2 being removeVertex of aT,v;
((T2 .order()) + 1) - 1 = (k + 1) - 1 by A7, GLIB_000:51;
then A8: k = (T2 .size()) + 1 by A6;
card (v .edgesInOut()) = v .degree() by GLIB_000:22
.= 1 by GLIB_000:def 54 ;
hence k + 1 = (T .size()) + 1 by A8, GLIB_000:51; :: thesis: verum

end;

then A9: 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(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

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 that
A13: G .order() = k + 1 and
A14: 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, A14, CARD_1:47, GLIB_000:def 27;
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;
consider G2 being removeVertex of G,v;
A16: ( (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 A15, GLIB_000:def 54 ;
then A17: G2 is connected by A12, A13, A14, A16;
consider e being set such that
A18: v .edgesInOut() = {e} and
A19: not e Joins v,v,G by A15, GLIB_000:def 53;
e in v .edgesInOut() by A18, TARSKI:def 1;
hence G is connected by A17, A19, Th3; :: thesis: verum

end;

then A20: for k being non empty Nat st S₁[k] holds
S₁[k + 1] ;

now

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: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 A22, 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 A23: S₁[1] ;
for k being non empty Nat holds S₁[k] from NAT_1:sch 10(A23, A20);
then G is connected by A10, A11;
hence G is Tree-like by A10; :: thesis: verum