defpred S_{1}[ 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 ) )

A10: G is acyclic and

A11: G .order() = (G .size()) + 1 ; :: thesis: G is Tree-like

_{1}[k] holds

S_{1}[k + 1]
;

_{1}[1]
;

for k being non zero Nat holds S_{1}[k]
from NAT_1:sch 10(A23, A20);

then G is connected by A10, A11;

hence G is Tree-like by A10; :: thesis: verum

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 )

assume that defpred S_{2}[ 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

_{2}[1]
;

_{2}[k] holds

S_{2}[k + 1]
;

for k being non zero Nat holds S_{2}[k]
from NAT_1:sch 10(A5, A9);

hence G .order() = (G .size()) + 1 by A1; :: thesis: verum

end;$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

then A5:
S1 = (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 T .size() = 0 by GLIB_000:def 25;

hence 1 = (T .size()) + 1 ; :: thesis: verum

end;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;

now :: thesis: for e being object holds not e in the_Edges_of T

then
card (the_Edges_of T) = 0
by CARD_1:27, XBOOLE_0:def 1;given e being object such that A3:
e in the_Edges_of T
; :: thesis: contradiction

(the_Target_of T) . e in {v} by A2, A3, FUNCT_2:5;

then A4: (the_Target_of T) . e = v by TARSKI:def 1;

(the_Source_of T) . e in {v} by A2, A3, FUNCT_2:5;

then (the_Source_of T) . e = v by TARSKI:def 1;

then e Joins v,v,T by A3, A4, GLIB_000:def 13;

then T .walkOf (v,e,v) is Cycle-like by GLIB_001:156;

hence contradiction by Def2; :: thesis: verum

end;(the_Target_of T) . e in {v} by A2, A3, FUNCT_2:5;

then A4: (the_Target_of T) . e = v by TARSKI:def 1;

(the_Source_of T) . e in {v} by A2, A3, FUNCT_2:5;

then (the_Source_of T) . e = v by TARSKI:def 1;

then e Joins v,v,T by A3, A4, GLIB_000:def 13;

then T .walkOf (v,e,v) is Cycle-like by GLIB_001:156;

hence contradiction by Def2; :: thesis: verum

then T .size() = 0 by GLIB_000:def 25;

hence 1 = (T .size()) + 1 ; :: thesis: verum

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

then A9:
for k being non zero Nat st Sk = (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;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

S

for k being non zero Nat holds S

hence G .order() = (G .size()) + 1 by A1; :: thesis: verum

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

then A20:
for k being non zero Nat st SG 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

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;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

then reconsider aG = G as _finite non _trivial acyclic _Graph by GLIB_000:26;assume
G .order() = 1
; :: thesis: contradiction

then 0 + 1 = k + 1 by A13;

hence contradiction ; :: thesis: verum

end;then 0 + 1 = k + 1 by A13;

hence contradiction ; :: thesis: verum

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

S

now :: thesis: for G being _finite acyclic _Graph st G .order() = 1 & G .order() = (G .size()) + 1 holds

G is connected

then A23:
SG 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;

end;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

hence
G is connected
; :: thesis: verumlet 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;( 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

for k being non zero Nat holds S

then G is connected by A10, A11;

hence G is Tree-like by A10; :: thesis: verum