:: GLIB_002 semantic presentation

begin

definition
let G be _Graph;
attrG is connected  means :Def1: :: GLIB_002:def 1
 for u, v being Vertex of G ex W being Walk of G st W is_Walk_from u,v;
end;

:: deftheorem Def1 defines connected GLIB_002:def_1_:_
 for G being _Graph holds
( G is connected iff for u, v being Vertex of G ex W being Walk of G st W is_Walk_from u,v );

definition
let G be _Graph;
attrG is acyclic  means :Def2: :: GLIB_002:def 2
 for W being Walk of G holds not W is Cycle-like ;
end;

:: deftheorem Def2 defines acyclic GLIB_002:def_2_:_
 for G being _Graph holds
( G is acyclic iff for W being Walk of G holds not W is Cycle-like );

definition
let G be _Graph;
attrG is Tree-like  means :Def3: :: GLIB_002:def 3
( G is acyclic & G is connected );
end;

:: deftheorem Def3 defines Tree-like GLIB_002:def_3_:_
 for G being _Graph holds
( G is Tree-like iff ( G is acyclic & G is connected ) );

registration
cluster Relation-like NAT -defined Function-like V31() [Graph-like] trivial  ->  connected for set ;
coherence
 for b1 being _Graph st b1 is trivial holds
b1 is connected
proof
let G be _Graph; ::_thesis: ( G is trivial implies G is connected )
assume  G is trivial ; ::_thesis: G is connected
then consider x being Vertex of G such that
A1: the_Vertices_of G = {x} by GLIB_000:22;
now__::_thesis:_for_u,_v_being_Vertex_of_G_ex_W_being_Walk_of_G_st_W_is_Walk_from_u,v
set W = G .walkOf x;
let u, v be Vertex of G; ::_thesis: ex W being Walk of G st W is_Walk_from u,v
 ( u = x & v = x ) by A1, TARSKI:def_1;
then  G .walkOf x is_Walk_from u,v by GLIB_001:13;
hence  ex W being Walk of G st W is_Walk_from u,v ; ::_thesis: verum
end;
hence  G is connected by Def1; ::_thesis: verum
end;
end;

registration
cluster Relation-like NAT -defined Function-like V31() [Graph-like] loopless trivial  ->  Tree-like for set ;
coherence
 for b1 being _Graph st b1 is trivial & b1 is loopless holds
b1 is Tree-like
proof
let G be _Graph; ::_thesis: ( G is trivial & G is loopless implies G is Tree-like )
assume that
A1: G is trivial and
A2: G is loopless ; ::_thesis: G is Tree-like
now__::_thesis:_for_W_being_Walk_of_G_holds_not_W_is_Cycle-like
given W being Walk of G such that A3: W is Cycle-like ; ::_thesis: contradiction
 W .edges() <> {} by A3, GLIB_001:136;
then  ex e being set st e in W .edges() by XBOOLE_0:def_1;
hence  contradiction by A1, A2, GLIB_000:23; ::_thesis: verum
end;
then A4: G is acyclic by Def2;
reconsider G9 = G as trivial _Graph by A1;
 G9 is connected ;
hence  G is Tree-like by A4, Def3; ::_thesis: verum
end;
end;

registration
cluster Relation-like NAT -defined Function-like V31() [Graph-like] acyclic  ->  simple for set ;
coherence
 for b1 being _Graph st b1 is acyclic holds
b1 is simple
proof
let G be _Graph; ::_thesis: ( G is acyclic implies G is simple )
assume A1: for W being Walk of G holds not W is Cycle-like ; :: according to GLIB_002:def_2 ::_thesis: G is simple
now__::_thesis:_for_e_being_set_holds_
(_not_e_in_the_Edges_of_G_or_not_(the_Source_of_G)_._e_=_(the_Target_of_G)_._e_)
given e being set  such that A2: e in the_Edges_of G and
A3: (the_Source_of G) . e = (the_Target_of G) . e ; ::_thesis: contradiction
set v1 = (the_Source_of G) . e;
reconsider v1 = (the_Source_of G) . e as Vertex of G by A2, FUNCT_2:5;
set W = G .walkOf (v1,e,v1);
 e Joins v1,v1,G by A2, A3, GLIB_000:def_13;
then  len (G .walkOf (v1,e,v1)) = 3 by GLIB_001:14;
then  not G .walkOf (v1,e,v1) is trivial by GLIB_001:125;
then  G .walkOf (v1,e,v1) is Cycle-like by GLIB_001:def_31;
hence  contradiction by A1; ::_thesis: verum
end;
then A4: G is loopless by GLIB_000:def_18;
now__::_thesis:_for_e1,_e2,_v1,_v2_being_set_st_e1_Joins_v1,v2,G_&_e2_Joins_v1,v2,G_holds_
e1_=_e2
let e1, e2, v1, v2 be set ; ::_thesis: ( e1 Joins v1,v2,G & e2 Joins v1,v2,G implies e1 = e2 )
assume that
A5: e1 Joins v1,v2,G and
A6: e2 Joins v1,v2,G ; ::_thesis: e1 = e2
A7: e2 Joins v2,v1,G by A6, GLIB_000:14;
A8: v1 <> v2 by A4, A5, GLIB_000:18;
now__::_thesis:_(_e1_<>_e2_implies_(_(G_.walkOf_(v1,e1,v2))_.addEdge_e2_is_Path-like_&_contradiction_)_)
set W1 = G .walkOf (v1,e1,v2);
set W = (G .walkOf (v1,e1,v2)) .addEdge e2;
assume A9: e1 <> e2 ; ::_thesis: ( (G .walkOf (v1,e1,v2)) .addEdge e2 is Path-like & contradiction )
reconsider W1 = G .walkOf (v1,e1,v2) as Path of G ;
A10: W1 .last() = v2 by A5, GLIB_001:15;
then A11: ((G .walkOf (v1,e1,v2)) .addEdge e2) .last() = v1 by A7, GLIB_001:63;
A12: len W1 = 3 by A5, GLIB_001:14;
A13: now__::_thesis:_for_n_being_odd_Element_of_NAT_st_1_<_n_&_n_<=_len_W1_holds_
W1_._n_<>_v1
let n be odd Element of NAT ; ::_thesis: ( 1 < n & n <= len W1 implies W1 . n <> v1 )
assume that
A14: 1 < n and
A15: n <= len W1 ; ::_thesis: W1 . n <> v1
 1 + 1 <= n by A14, NAT_1:13;
then  2 * 1 < n by XXREAL_0:1;
then  (2 * 1) + 1 <= n by NAT_1:13;
then A16: n = 3 by A12, A15, XXREAL_0:1;
 W1 = <*v1,e1,v2*> by A5, GLIB_001:def_5;
hence  W1 . n <> v1 by A8, A16, FINSEQ_1:45; ::_thesis: verum
end;
 ( W1 .first() = v1 & W1 .last() = v2 ) by A5, GLIB_001:15;
then A17: W1 is open by A8, GLIB_001:def_24;
 W1 .first() = v1 by A5, GLIB_001:15;
then  ((G .walkOf (v1,e1,v2)) .addEdge e2) .first() = v1 by A7, A10, GLIB_001:63;
then A18: (G .walkOf (v1,e1,v2)) .addEdge e2 is closed by A11, GLIB_001:def_24;
A19: e2 Joins W1 .last() ,v1,G by A5, A7, GLIB_001:15;
then A20: not (G .walkOf (v1,e1,v2)) .addEdge e2 is trivial by GLIB_001:132;
 W1 .edges() = {e1} by A5, GLIB_001:108;
then  not e2 in W1 .edges() by A9, TARSKI:def_1;
hence  (G .walkOf (v1,e1,v2)) .addEdge e2 is Path-like by A19, A17, A13, GLIB_001:150; ::_thesis: contradiction
then  (G .walkOf (v1,e1,v2)) .addEdge e2 is Cycle-like by A18, A20, GLIB_001:def_31;
hence  contradiction by A1; ::_thesis: verum
end;
hence  e1 = e2 ; ::_thesis: verum
end;
then  G is non-multi by GLIB_000:def_20;
hence  G is simple by A4; ::_thesis: verum
end;
end;

registration
cluster Relation-like NAT -defined Function-like V31() [Graph-like] Tree-like  ->  connected acyclic for set ;
coherence
 for b1 being _Graph st b1 is Tree-like holds
( b1 is acyclic & b1 is connected ) by Def3;
end;

registration
cluster Relation-like NAT -defined Function-like V31() [Graph-like] connected acyclic  ->  Tree-like for set ;
coherence
 for b1 being _Graph st b1 is acyclic & b1 is connected holds
b1 is Tree-like by Def3;
end;

registration
let G be _Graph;
let v be Vertex of G;
cluster  ->  Tree-like for inducedSubgraph of G,{v}, {} ;
coherence
 for b1 being inducedSubgraph of G,{v}, {} holds b1 is Tree-like ;
end;

definition
let G be _Graph;
let v be set ;
predG is_DTree_rooted_at v means :Def4: :: GLIB_002:def 4
( G is Tree-like & ( for x being Vertex of G ex W being DWalk of G st W is_Walk_from v,x ) );
end;

:: deftheorem Def4 defines is_DTree_rooted_at GLIB_002:def_4_:_
 for G being _Graph
for v being set holds
( G is_DTree_rooted_at v iff ( G is Tree-like & ( for x being Vertex of G ex W being DWalk of G st W is_Walk_from v,x ) ) );

registration
cluster Relation-like NAT -defined Function-like V31() [Graph-like] finite trivial Tree-like for set ;
existence
 ex b1 being _Graph st
( b1 is trivial & b1 is finite & b1 is Tree-like )
proof
set V = {1};
set E = {} ;
reconsider S = {} as Function of {},{1} by RELSET_1:12;
set G = createGraph ({1},{},S,S);
take  createGraph ({1},{},S,S) ; ::_thesis: ( createGraph ({1},{},S,S) is trivial & createGraph ({1},{},S,S) is finite & createGraph ({1},{},S,S) is Tree-like )
thus  ( createGraph ({1},{},S,S) is trivial & createGraph ({1},{},S,S) is finite & createGraph ({1},{},S,S) is Tree-like ) ; ::_thesis: verum
end;
cluster Relation-like NAT -defined Function-like V31() [Graph-like] finite non trivial Tree-like for set ;
existence
 ex b1 being _Graph st
( not b1 is trivial & b1 is finite & b1 is Tree-like )
proof
set V = {0,1};
set E = {0};
set S = 0 .--> 0;
set T = 0 .--> 1;
A1: dom (0 .--> 1) = {0} by FUNCOP_1:13;
A2: now__::_thesis:_for_x_being_set_st_x_in_{0}_holds_
(0_.-->_1)_._x_in_{0,1}
let x be set ; ::_thesis: ( x in {0} implies (0 .--> 1) . x in {0,1} )
assume  x in {0} ; ::_thesis: (0 .--> 1) . x in {0,1}
then  x = 0 by TARSKI:def_1;
then  (0 .--> 1) . x = 1 by FUNCOP_1:72;
hence  (0 .--> 1) . x in {0,1} by TARSKI:def_2; ::_thesis: verum
end;
A3: now__::_thesis:_for_x_being_set_st_x_in_{0}_holds_
(0_.-->_0)_._x_in_{0,1}
let x be set ; ::_thesis: ( x in {0} implies (0 .--> 0) . x in {0,1} )
assume  x in {0} ; ::_thesis: (0 .--> 0) . x in {0,1}
then  x = 0 by TARSKI:def_1;
then  (0 .--> 0) . x = 0 by FUNCOP_1:72;
hence  (0 .--> 0) . x in {0,1} by TARSKI:def_2; ::_thesis: verum
end;
reconsider T = 0 .--> 1 as Function of {0},{0,1} by A1, A2, FUNCT_2:3;
 dom (0 .--> 0) = {0} by FUNCOP_1:13;
then reconsider S = 0 .--> 0 as Function of {0},{0,1} by A3, FUNCT_2:3;
set G = createGraph ({0,1},{0},S,T);
A4: the_Edges_of (createGraph ({0,1},{0},S,T)) = {0} by GLIB_000:6;
 the_Target_of (createGraph ({0,1},{0},S,T)) = T by GLIB_000:6;
then A5: (the_Target_of (createGraph ({0,1},{0},S,T))) . 0 = 1 by FUNCOP_1:72;
 the_Source_of (createGraph ({0,1},{0},S,T)) = S by GLIB_000:6;
then A6: (the_Source_of (createGraph ({0,1},{0},S,T))) . 0 = 0 by FUNCOP_1:72;
now__::_thesis:_for_W_being_Walk_of_createGraph_({0,1},{0},S,T)_holds_not_W_is_Cycle-like
given W being Walk of createGraph ({0,1},{0},S,T) such that A7: W is Cycle-like ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( len W = 3 or len W <> 3 ) ;
supposeA8: len W = 3 ; ::_thesis: contradiction
set e = W . (1 + 1);
set v1 = W . 1;
set v2 = W . (1 + 2);
A9: W . (1 + 1) Joins W . 1,W . (1 + 2), createGraph ({0,1},{0},S,T) by A8, GLIB_001:def_3, JORDAN12:2;
 W . 1 = W . (1 + 2) by A7, A8, GLIB_001:118;
then A10: ( ( (the_Source_of (createGraph ({0,1},{0},S,T))) . (W . (1 + 1)) = W . 1 & (the_Target_of (createGraph ({0,1},{0},S,T))) . (W . (1 + 1)) = W . 1 ) or ( (the_Source_of (createGraph ({0,1},{0},S,T))) . (W . (1 + 1)) = W . 1 & (the_Target_of (createGraph ({0,1},{0},S,T))) . (W . (1 + 1)) = W . 1 ) ) by A9, GLIB_000:def_13;
 W . (1 + 1) in the_Edges_of (createGraph ({0,1},{0},S,T)) by A9, GLIB_000:def_13;
then  ( ( W . 1 = 0 & W . 1 = 1 ) or ( W . 1 = 1 & W . 1 = 0 ) ) by A4, A6, A5, A10, TARSKI:def_1;
hence  contradiction ; ::_thesis: verum
end;
supposeA11: len W <> 3 ; ::_thesis: contradiction
A12: 3 <= len W by A7, GLIB_001:125;
then  3 - 1 <= (len W) - 0 by XREAL_1:13;
then  2 * 1 in dom W by FINSEQ_3:25;
then  W . (2 * 1) in {0} by A4, GLIB_001:8;
then A13: W . (2 * 1) = 0 by TARSKI:def_1;
 3 < len W by A11, A12, XXREAL_0:1;
then A14: 3 + 1 <= len W by NAT_1:13;
then  2 * 2 in dom W by FINSEQ_3:25;
then  W . (2 * 2) in {0} by A4, GLIB_001:8;
then  W . (2 * 2) = 0 by TARSKI:def_1;
hence  contradiction by A7, A14, A13, GLIB_001:138; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
then A15: createGraph ({0,1},{0},S,T) is acyclic by Def2;
set W1 = (createGraph ({0,1},{0},S,T)) .walkOf (0,0,1);
set W2 = ((createGraph ({0,1},{0},S,T)) .walkOf (0,0,1)) .reverse() ;
take  createGraph ({0,1},{0},S,T) ; ::_thesis: ( not createGraph ({0,1},{0},S,T) is trivial & createGraph ({0,1},{0},S,T) is finite & createGraph ({0,1},{0},S,T) is Tree-like )
A16: the_Vertices_of (createGraph ({0,1},{0},S,T)) = {0,1} by GLIB_000:6;
then reconsider a0 = 0 , a1 = 1 as Vertex of (createGraph ({0,1},{0},S,T)) by TARSKI:def_2;
now__::_thesis:_not_card_(the_Vertices_of_(createGraph_({0,1},{0},S,T)))_=_1
assume  card (the_Vertices_of (createGraph ({0,1},{0},S,T))) = 1 ; ::_thesis: contradiction
then  ex x being set st the_Vertices_of (createGraph ({0,1},{0},S,T)) = {x} by CARD_2:42;
hence  contradiction by A16, ZFMISC_1:5; ::_thesis: verum
end;
hence  ( not createGraph ({0,1},{0},S,T) is trivial & createGraph ({0,1},{0},S,T) is finite ) by GLIB_000:def_19; ::_thesis: createGraph ({0,1},{0},S,T) is Tree-like
 0 in the_Edges_of (createGraph ({0,1},{0},S,T)) by A4, TARSKI:def_1;
then  0 Joins 0 ,1, createGraph ({0,1},{0},S,T) by A6, A5, GLIB_000:def_13;
then A17: (createGraph ({0,1},{0},S,T)) .walkOf (0,0,1) is_Walk_from 0 ,1 by GLIB_001:15;
then A18: ((createGraph ({0,1},{0},S,T)) .walkOf (0,0,1)) .reverse() is_Walk_from 1, 0 by GLIB_001:23;
now__::_thesis:_for_u,_v_being_Vertex_of_(createGraph_({0,1},{0},S,T))_ex_W_being_Walk_of_createGraph_({0,1},{0},S,T)_st_W_is_Walk_from_u,v
let u, v be Vertex of (createGraph ({0,1},{0},S,T)); ::_thesis: ex W being Walk of createGraph ({0,1},{0},S,T) st W is_Walk_from u,v
now__::_thesis:_ex_W_being_Walk_of_createGraph_({0,1},{0},S,T)_st_W_is_Walk_from_u,v
percases ( ( u = 0 & v = 0 ) or ( u = 0 & v = 1 ) or ( u = 1 & v = 0 ) or ( u = 1 & v = 1 ) ) by A16, TARSKI:def_2;
suppose ( u = 0 & v = 0 ) ; ::_thesis: ex W being Walk of createGraph ({0,1},{0},S,T) st W is_Walk_from u,v
then  (createGraph ({0,1},{0},S,T)) .walkOf a0 is_Walk_from u,v by GLIB_001:13;
hence  ex W being Walk of createGraph ({0,1},{0},S,T) st W is_Walk_from u,v ; ::_thesis: verum
end;
suppose ( u = 0 & v = 1 ) ; ::_thesis: ex W being Walk of createGraph ({0,1},{0},S,T) st W is_Walk_from u,v
hence  ex W being Walk of createGraph ({0,1},{0},S,T) st W is_Walk_from u,v by A17; ::_thesis: verum
end;
suppose ( u = 1 & v = 0 ) ; ::_thesis: ex W being Walk of createGraph ({0,1},{0},S,T) st W is_Walk_from u,v
hence  ex W being Walk of createGraph ({0,1},{0},S,T) st W is_Walk_from u,v by A18; ::_thesis: verum
end;
suppose ( u = 1 & v = 1 ) ; ::_thesis: ex W being Walk of createGraph ({0,1},{0},S,T) st W is_Walk_from u,v
then  (createGraph ({0,1},{0},S,T)) .walkOf a1 is_Walk_from u,v by GLIB_001:13;
hence  ex W being Walk of createGraph ({0,1},{0},S,T) st W is_Walk_from u,v ; ::_thesis: verum
end;
end;
end;
hence  ex W being Walk of createGraph ({0,1},{0},S,T) st W is_Walk_from u,v ; ::_thesis: verum
end;
then  createGraph ({0,1},{0},S,T) is connected by Def1;
hence  createGraph ({0,1},{0},S,T) is Tree-like by A15; ::_thesis: verum
end;
end;

registration
let G be _Graph;
cluster Relation-like NAT -defined Function-like V31() [Graph-like] finite trivial Tree-like for Subgraph of G;
existence
 ex b1 being Subgraph of G st
( b1 is trivial & b1 is finite & b1 is Tree-like )
proof
set IT = the finite trivial simple Subgraph of G;
take  the finite trivial simple Subgraph of G ; ::_thesis: ( the finite trivial simple Subgraph of G is trivial & the finite trivial simple Subgraph of G is finite & the finite trivial simple Subgraph of G is Tree-like )
thus  ( the finite trivial simple Subgraph of G is trivial & the finite trivial simple Subgraph of G is finite & the finite trivial simple Subgraph of G is Tree-like ) ; ::_thesis: verum
end;
end;

registration
let G be acyclic _Graph;
cluster  ->  acyclic for Subgraph of G;
coherence
 for b1 being Subgraph of G holds b1 is acyclic
proof
let G2 be Subgraph of G; ::_thesis: G2 is acyclic
now__::_thesis:_for_W2_being_Walk_of_G2_holds_not_W2_is_Cycle-like
given W2 being Walk of G2 such that A1: W2 is Cycle-like ; ::_thesis: contradiction
reconsider W = W2 as Walk of G by GLIB_001:167;
A2: W is Path-like by A1, GLIB_001:176;
 ( W is closed & not W is trivial ) by A1, GLIB_001:176;
then  W is Cycle-like by A2, GLIB_001:def_31;
hence  contradiction by Def2; ::_thesis: verum
end;
hence  G2 is acyclic by Def2; ::_thesis: verum
end;
end;

definition
let G be _Graph;
let v be Vertex of G;
funcG .reachableFrom v ->  non empty Subset of (the_Vertices_of G) means :Def5: :: GLIB_002:def 5
 for x being set holds
( x in it iff ex W being Walk of G st W is_Walk_from v,x );
existence
 ex b1 being non empty Subset of (the_Vertices_of G) st
for x being set holds
( x in b1 iff ex W being Walk of G st W is_Walk_from v,x )
proof
defpred S1[ set ] means  ex W being Walk of G st W is_Walk_from v,$1;
consider IT being Subset of (the_Vertices_of G) such that
A1: for x being set holds
( x in IT iff ( x in the_Vertices_of G & S1[x] ) ) from SUBSET_1:sch_1();
 G .walkOf v is_Walk_from v,v by GLIB_001:13;
then reconsider IT = IT as non empty Subset of (the_Vertices_of G) by A1;
take  IT ; ::_thesis: for x being set holds
( x in IT iff ex W being Walk of G st W is_Walk_from v,x )
let x be set ; ::_thesis: ( x in IT iff ex W being Walk of G st W is_Walk_from v,x )
thus  ( x in IT implies ex W being Walk of G st W is_Walk_from v,x ) by A1; ::_thesis: ( ex W being Walk of G st W is_Walk_from v,x implies x in IT )
assume A2: ex W being Walk of G st W is_Walk_from v,x ; ::_thesis: x in IT
then  x is Vertex of G by GLIB_001:18;
hence  x in IT by A1, A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being non empty Subset of (the_Vertices_of G) st ( for x being set holds
( x in b1 iff ex W being Walk of G st W is_Walk_from v,x ) ) & ( for x being set holds
( x in b2 iff ex W being Walk of G st W is_Walk_from v,x ) ) holds
b1 = b2
proof
let IT1, IT2 be non empty Subset of (the_Vertices_of G); ::_thesis: ( ( for x being set holds
( x in IT1 iff ex W being Walk of G st W is_Walk_from v,x ) ) & ( for x being set holds
( x in IT2 iff ex W being Walk of G st W is_Walk_from v,x ) ) implies IT1 = IT2 )
assume that
A3: for x being set holds
( x in IT1 iff ex W being Walk of G st W is_Walk_from v,x ) and
A4: for x being set holds
( x in IT2 iff ex W being Walk of G st W is_Walk_from v,x ) ; ::_thesis: IT1 = IT2
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_IT1_implies_x_in_IT2_)_&_(_x_in_IT2_implies_x_in_IT1_)_)
let x be set ; ::_thesis: ( ( x in IT1 implies x in IT2 ) & ( x in IT2 implies x in IT1 ) )
hereby  ::_thesis: ( x in IT2 implies x in IT1 )
assume  x in IT1 ; ::_thesis: x in IT2
then  ex W being Walk of G st W is_Walk_from v,x by A3;
hence  x in IT2 by A4; ::_thesis: verum
end;
assume  x in IT2 ; ::_thesis: x in IT1
then  ex W being Walk of G st W is_Walk_from v,x by A4;
hence  x in IT1 by A3; ::_thesis: verum
end;
hence  IT1 = IT2 by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines .reachableFrom GLIB_002:def_5_:_
 for G being _Graph
for v being Vertex of G
for b3 being non empty Subset of (the_Vertices_of G) holds
( b3 = G .reachableFrom v iff for x being set holds
( x in b3 iff ex W being Walk of G st W is_Walk_from v,x ) );

definition
let G be _Graph;
let v be Vertex of G;
funcG .reachableDFrom v ->  non empty Subset of (the_Vertices_of G) means :Def6: :: GLIB_002:def 6
 for x being set holds
( x in it iff ex W being DWalk of G st W is_Walk_from v,x );
existence
 ex b1 being non empty Subset of (the_Vertices_of G) st
for x being set holds
( x in b1 iff ex W being DWalk of G st W is_Walk_from v,x )
proof
set W = G .walkOf v;
defpred S1[ set ] means  ex W being directed Walk of G st W is_Walk_from v,$1;
consider IT being Subset of (the_Vertices_of G) such that
A1: for x being set holds
( x in IT iff ( x in the_Vertices_of G & S1[x] ) ) from SUBSET_1:sch_1();
 G .walkOf v is_Walk_from v,v by GLIB_001:13;
then reconsider IT = IT as non empty Subset of (the_Vertices_of G) by A1;
take  IT ; ::_thesis: for x being set holds
( x in IT iff ex W being DWalk of G st W is_Walk_from v,x )
let x be set ; ::_thesis: ( x in IT iff ex W being DWalk of G st W is_Walk_from v,x )
thus  ( x in IT implies ex W being directed Walk of G st W is_Walk_from v,x ) by A1; ::_thesis: ( ex W being DWalk of G st W is_Walk_from v,x implies x in IT )
given W being directed Walk of G such that A2: W is_Walk_from v,x ; ::_thesis: x in IT
 x is Vertex of G by A2, GLIB_001:18;
hence  x in IT by A1, A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being non empty Subset of (the_Vertices_of G) st ( for x being set holds
( x in b1 iff ex W being DWalk of G st W is_Walk_from v,x ) ) & ( for x being set holds
( x in b2 iff ex W being DWalk of G st W is_Walk_from v,x ) ) holds
b1 = b2
proof
let IT1, IT2 be non empty Subset of (the_Vertices_of G); ::_thesis: ( ( for x being set holds
( x in IT1 iff ex W being DWalk of G st W is_Walk_from v,x ) ) & ( for x being set holds
( x in IT2 iff ex W being DWalk of G st W is_Walk_from v,x ) ) implies IT1 = IT2 )
assume that
A3: for x being set holds
( x in IT1 iff ex W being directed Walk of G st W is_Walk_from v,x ) and
A4: for x being set holds
( x in IT2 iff ex W being directed Walk of G st W is_Walk_from v,x ) ; ::_thesis: IT1 = IT2
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_IT1_implies_x_in_IT2_)_&_(_x_in_IT2_implies_x_in_IT1_)_)
let x be set ; ::_thesis: ( ( x in IT1 implies x in IT2 ) & ( x in IT2 implies x in IT1 ) )
hereby  ::_thesis: ( x in IT2 implies x in IT1 )
assume  x in IT1 ; ::_thesis: x in IT2
then  ex W being directed Walk of G st W is_Walk_from v,x by A3;
hence  x in IT2 by A4; ::_thesis: verum
end;
assume  x in IT2 ; ::_thesis: x in IT1
then  ex W being directed Walk of G st W is_Walk_from v,x by A4;
hence  x in IT1 by A3; ::_thesis: verum
end;
hence  IT1 = IT2 by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines .reachableDFrom GLIB_002:def_6_:_
 for G being _Graph
for v being Vertex of G
for b3 being non empty Subset of (the_Vertices_of G) holds
( b3 = G .reachableDFrom v iff for x being set holds
( x in b3 iff ex W being DWalk of G st W is_Walk_from v,x ) );

Lm1:  for G being _Graph
for v being Vertex of G holds v in G .reachableFrom v
proof
let G be _Graph; ::_thesis: for v being Vertex of G holds v in G .reachableFrom v
let v be Vertex of G; ::_thesis: v in G .reachableFrom v
 G .walkOf v is_Walk_from v,v by GLIB_001:13;
hence  v in G .reachableFrom v by Def5; ::_thesis: verum
end;

Lm2:  for G being _Graph
for v1 being Vertex of G
for e, x, y being set st x in G .reachableFrom v1 & e Joins x,y,G holds
y in G .reachableFrom v1
proof
let G be _Graph; ::_thesis: for v1 being Vertex of G
for e, x, y being set st x in G .reachableFrom v1 & e Joins x,y,G holds
y in G .reachableFrom v1
let v1 be Vertex of G; ::_thesis: for e, x, y being set st x in G .reachableFrom v1 & e Joins x,y,G holds
y in G .reachableFrom v1
let e, x, y be set ; ::_thesis: ( x in G .reachableFrom v1 & e Joins x,y,G implies y in G .reachableFrom v1 )
set RFV = G .reachableFrom v1;
assume that
A1: x in G .reachableFrom v1 and
A2: e Joins x,y,G ; ::_thesis: y in G .reachableFrom v1
consider W being Walk of G such that
A3: W is_Walk_from v1,x by A1, Def5;
 W .addEdge e is_Walk_from v1,y by A2, A3, GLIB_001:66;
hence  y in G .reachableFrom v1 by Def5; ::_thesis: verum
end;

Lm3:  for G being _Graph
for v1, v2 being Vertex of G st v1 in G .reachableFrom v2 holds
G .reachableFrom v1 = G .reachableFrom v2
proof
let G be _Graph; ::_thesis: for v1, v2 being Vertex of G st v1 in G .reachableFrom v2 holds
G .reachableFrom v1 = G .reachableFrom v2
let v1, v2 be Vertex of G; ::_thesis: ( v1 in G .reachableFrom v2 implies G .reachableFrom v1 = G .reachableFrom v2 )
assume  v1 in G .reachableFrom v2 ; ::_thesis: G .reachableFrom v1 = G .reachableFrom v2
then consider WA being Walk of G such that
A1: WA is_Walk_from v2,v1 by Def5;
A2: WA .reverse() is_Walk_from v1,v2 by A1, GLIB_001:23;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_G_.reachableFrom_v1_implies_x_in_G_.reachableFrom_v2_)_&_(_x_in_G_.reachableFrom_v2_implies_x_in_G_.reachableFrom_v1_)_)
let x be set ; ::_thesis: ( ( x in G .reachableFrom v1 implies x in G .reachableFrom v2 ) & ( x in G .reachableFrom v2 implies x in G .reachableFrom v1 ) )
hereby  ::_thesis: ( x in G .reachableFrom v2 implies x in G .reachableFrom v1 )
assume  x in G .reachableFrom v1 ; ::_thesis: x in G .reachableFrom v2
then consider WB being Walk of G such that
A3: WB is_Walk_from v1,x by Def5;
 WA .append WB is_Walk_from v2,x by A1, A3, GLIB_001:31;
hence  x in G .reachableFrom v2 by Def5; ::_thesis: verum
end;
assume  x in G .reachableFrom v2 ; ::_thesis: x in G .reachableFrom v1
then consider WB being Walk of G such that
A4: WB is_Walk_from v2,x by Def5;
 (WA .reverse()) .append WB is_Walk_from v1,x by A2, A4, GLIB_001:31;
hence  x in G .reachableFrom v1 by Def5; ::_thesis: verum
end;
hence  G .reachableFrom v1 = G .reachableFrom v2 by TARSKI:1; ::_thesis: verum
end;

Lm4:  for G being _Graph
for W being Walk of G
for v being Vertex of G st v in W .vertices() holds
W .vertices() c= G .reachableFrom v
proof
let G be _Graph; ::_thesis: for W being Walk of G
for v being Vertex of G st v in W .vertices() holds
W .vertices() c= G .reachableFrom v
let W be Walk of G; ::_thesis: for v being Vertex of G st v in W .vertices() holds
W .vertices() c= G .reachableFrom v
let v be Vertex of G; ::_thesis: ( v in W .vertices() implies W .vertices() c= G .reachableFrom v )
assume  v in W .vertices() ; ::_thesis: W .vertices() c= G .reachableFrom v
then consider m being odd Element of NAT  such that
A1: m <= len W and
A2: W . m = v by GLIB_001:87;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in W .vertices() or x in G .reachableFrom v )
assume  x in W .vertices() ; ::_thesis: x in G .reachableFrom v
then consider n being odd Element of NAT  such that
A3: n <= len W and
A4: W . n = x by GLIB_001:87;
now__::_thesis:_ex_W2_being_Walk_of_G_st_W2_is_Walk_from_v,x
percases ( m <= n or m > n ) ;
suppose m <= n ; ::_thesis: ex W2 being Walk of G st W2 is_Walk_from v,x
then  W .cut (m,n) is_Walk_from v,x by A2, A3, A4, GLIB_001:37;
hence  ex W2 being Walk of G st W2 is_Walk_from v,x ; ::_thesis: verum
end;
suppose m > n ; ::_thesis: ex W2 being Walk of G st W2 is_Walk_from v,x
then  W .cut (n,m) is_Walk_from x,v by A1, A2, A4, GLIB_001:37;
then  (W .cut (n,m)) .reverse() is_Walk_from v,x by GLIB_001:23;
hence  ex W2 being Walk of G st W2 is_Walk_from v,x ; ::_thesis: verum
end;
end;
end;
hence  x in G .reachableFrom v by Def5; ::_thesis: verum
end;

definition
let G1 be _Graph;
let G2 be Subgraph of G1;
attrG2 is Component-like  means :Def7: :: GLIB_002:def 7
( G2 is connected & ( for G3 being connected Subgraph of G1 holds not G2 c< G3 ) );
end;

:: deftheorem Def7 defines Component-like GLIB_002:def_7_:_
 for G1 being _Graph
for G2 being Subgraph of G1 holds
( G2 is Component-like iff ( G2 is connected & ( for G3 being connected Subgraph of G1 holds not G2 c< G3 ) ) );

registration
let G be _Graph;
cluster Component-like  ->  connected for Subgraph of G;
coherence
 for b1 being Subgraph of G st b1 is Component-like holds
b1 is connected by Def7;
end;

registration
let G be _Graph;
let v be Vertex of G;
cluster  ->  Component-like for inducedSubgraph of G,G .reachableFrom v,G .edgesBetween (G .reachableFrom v);
coherence
 for b1 being inducedSubgraph of G,(G .reachableFrom v) holds b1 is Component-like
proof
let G2 be inducedSubgraph of G,(G .reachableFrom v); ::_thesis: G2 is Component-like
A1: the_Vertices_of G2 = G .reachableFrom v by GLIB_000:def_37;
A2: the_Edges_of G2 = G .edgesBetween (G .reachableFrom v) by GLIB_000:def_37;
A3: now__::_thesis:_for_G3_being_connected_Subgraph_of_G_holds_not_G2_c<_G3
A4: v in the_Vertices_of G2 by A1, Lm1;
given G3 being connected Subgraph of G such that A5: G2 c< G3 ; ::_thesis: contradiction
 G2 c= G3 by A5, GLIB_000:def_36;
then A6: G2 is Subgraph of G3 by GLIB_000:def_35;
then A7: the_Vertices_of G2 c= the_Vertices_of G3 by GLIB_000:def_32;
A8: now__::_thesis:_for_x_being_set_holds_
(_not_x_in_the_Vertices_of_G3_or_x_in_the_Vertices_of_G2_)
given x being set  such that A9: x in the_Vertices_of G3 and
A10: not x in the_Vertices_of G2 ; ::_thesis: contradiction
consider W being Walk of G3 such that
A11: W is_Walk_from v,x by A4, A7, A9, Def1;
reconsider W = W as Walk of G by GLIB_001:167;
 W is_Walk_from v,x by A11, GLIB_001:19;
hence  contradiction by A1, A10, Def5; ::_thesis: verum
end;
A12: the_Vertices_of G2 c= the_Vertices_of G3 by A6, GLIB_000:def_32;
now__::_thesis:_contradiction
percases ( ex x being set st
( x in the_Vertices_of G3 & not x in the_Vertices_of G2 ) or ex e being set st
( e in the_Edges_of G3 & not e in the_Edges_of G2 ) ) by A5, GLIB_000:99;
suppose ex x being set st
( x in the_Vertices_of G3 & not x in the_Vertices_of G2 ) ; ::_thesis: contradiction
hence  contradiction by A8; ::_thesis: verum
end;
suppose ex e being set st
( e in the_Edges_of G3 & not e in the_Edges_of G2 ) ; ::_thesis: contradiction
then consider e being set  such that
A13: e in the_Edges_of G3 and
A14: not e in the_Edges_of G2 ;
set v1 = (the_Source_of G3) . e;
set v2 = (the_Target_of G3) . e;
A15: e Joins (the_Source_of G3) . e,(the_Target_of G3) . e,G3 by A13, GLIB_000:def_13;
then A16: e Joins (the_Source_of G3) . e,(the_Target_of G3) . e,G by GLIB_000:72;
now__::_thesis:_contradiction
percases ( the_Vertices_of G3 = the_Vertices_of G2 or the_Vertices_of G3 <> the_Vertices_of G2 ) ;
suppose the_Vertices_of G3 = the_Vertices_of G2 ; ::_thesis: contradiction
then reconsider v1 = (the_Source_of G3) . e, v2 = (the_Target_of G3) . e as Vertex of G2 by A15, GLIB_000:13;
 ( v1 in G .reachableFrom v & v2 in G .reachableFrom v ) by A1;
hence  contradiction by A2, A14, A16, GLIB_000:32; ::_thesis: verum
end;
suppose the_Vertices_of G3 <> the_Vertices_of G2 ; ::_thesis: contradiction
then  the_Vertices_of G2 c< the_Vertices_of G3 by A12, XBOOLE_0:def_8;
hence  contradiction by A8, XBOOLE_0:6; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
now__::_thesis:_for_x,_y_being_Vertex_of_G2_ex_W_being_Walk_of_G2_st_W_is_Walk_from_x,y
let x, y be Vertex of G2; ::_thesis: ex W being Walk of G2 st W is_Walk_from x,y
consider W1R being Walk of G such that
A17: W1R is_Walk_from v,x by A1, Def5;
consider W2 being Walk of G such that
A18: W2 is_Walk_from v,y by A1, Def5;
set W1 = W1R .reverse() ;
set W = (W1R .reverse()) .append W2;
A19: W1R .reverse() is_Walk_from x,v by A17, GLIB_001:23;
then A20: (W1R .reverse()) .append W2 is_Walk_from x,y by A18, GLIB_001:31;
A21: (W1R .reverse()) .last() = v by A19, GLIB_001:def_23;
then A22: v in (W1R .reverse()) .vertices() by GLIB_001:88;
A23: ((W1R .reverse()) .append W2) .edges() c= G .edgesBetween (((W1R .reverse()) .append W2) .vertices()) by GLIB_001:109;
 W2 .first() = v by A18, GLIB_001:def_23;
then  ((W1R .reverse()) .append W2) .vertices() = ((W1R .reverse()) .vertices()) \/ (W2 .vertices()) by A21, GLIB_001:93;
then A24: v in ((W1R .reverse()) .append W2) .vertices() by A22, XBOOLE_0:def_3;
then  G .edgesBetween (((W1R .reverse()) .append W2) .vertices()) c= G .edgesBetween (the_Vertices_of G2) by A1, Lm4, GLIB_000:36;
then  ((W1R .reverse()) .append W2) .edges() c= G .edgesBetween (the_Vertices_of G2) by A23, XBOOLE_1:1;
then reconsider W = (W1R .reverse()) .append W2 as Walk of G2 by A1, A2, A24, Lm4, GLIB_001:170;
take W = W; ::_thesis: W is_Walk_from x,y
thus  W is_Walk_from x,y by A20, GLIB_001:19; ::_thesis: verum
end;
then  G2 is connected by Def1;
hence  G2 is Component-like by A3, Def7; ::_thesis: verum
end;
end;

registration
let G be _Graph;
cluster Relation-like NAT -defined Function-like V31() [Graph-like] Component-like for Subgraph of G;
existence
 ex b1 being Subgraph of G st b1 is Component-like
proof
set v = the Vertex of G;
set IT = the inducedSubgraph of G,(G .reachableFrom the Vertex of G);
take  the inducedSubgraph of G,(G .reachableFrom the Vertex of G) ; ::_thesis: the inducedSubgraph of G,(G .reachableFrom the Vertex of G) is Component-like
thus  the inducedSubgraph of G,(G .reachableFrom the Vertex of G) is Component-like ; ::_thesis: verum
end;
end;

definition
let G be _Graph;
mode Component of G is Component-like Subgraph of G;
end;

definition
let G be _Graph;
funcG .componentSet()  ->  non empty Subset-Family of (the_Vertices_of G) means :Def8: :: GLIB_002:def 8
 for x being set holds
( x in it iff ex v being Vertex of G st x = G .reachableFrom v );
existence
 ex b1 being non empty Subset-Family of (the_Vertices_of G) st
for x being set holds
( x in b1 iff ex v being Vertex of G st x = G .reachableFrom v )
proof
set v = the Vertex of G;
defpred S1[ set ] means  ex v being Vertex of G st $1 = G .reachableFrom v;
consider IT being Subset-Family of (the_Vertices_of G) such that
A1: for x being set holds
( x in IT iff ( x in bool (the_Vertices_of G) & S1[x] ) ) from SUBSET_1:sch_1();
set x = G .reachableFrom the Vertex of G;
 G .reachableFrom the Vertex of G in IT by A1;
then reconsider IT = IT as non empty Subset-Family of (the_Vertices_of G) ;
take  IT ; ::_thesis: for x being set holds
( x in IT iff ex v being Vertex of G st x = G .reachableFrom v )
thus  for x being set holds
( x in IT iff ex v being Vertex of G st x = G .reachableFrom v ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being non empty Subset-Family of (the_Vertices_of G) st ( for x being set holds
( x in b1 iff ex v being Vertex of G st x = G .reachableFrom v ) ) & ( for x being set holds
( x in b2 iff ex v being Vertex of G st x = G .reachableFrom v ) ) holds
b1 = b2
proof
defpred S1[ set ] means  ex v being Vertex of G st $1 = G .reachableFrom v;
let IT1, IT2 be non empty Subset-Family of (the_Vertices_of G); ::_thesis: ( ( for x being set holds
( x in IT1 iff ex v being Vertex of G st x = G .reachableFrom v ) ) & ( for x being set holds
( x in IT2 iff ex v being Vertex of G st x = G .reachableFrom v ) ) implies IT1 = IT2 )
assume that
A2: for x being set holds
( x in IT1 iff S1[x] ) and
A3: for x being set holds
( x in IT2 iff S1[x] ) ; ::_thesis: IT1 = IT2
now__::_thesis:_for_x_being_set_holds_
(_x_in_IT1_iff_x_in_IT2_)
let x be set ; ::_thesis: ( x in IT1 iff x in IT2 )
 ( x in IT1 iff S1[x] ) by A2;
hence  ( x in IT1 iff x in IT2 ) by A3; ::_thesis: verum
end;
hence  IT1 = IT2 by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines .componentSet() GLIB_002:def_8_:_
 for G being _Graph
for b2 being non empty Subset-Family of (the_Vertices_of G) holds
( b2 = G .componentSet() iff for x being set holds
( x in b2 iff ex v being Vertex of G st x = G .reachableFrom v ) );

registration
let G be _Graph;
let X be Element of G .componentSet() ;
cluster  ->  Component-like for inducedSubgraph of G,X,G .edgesBetween X;
coherence
 for b1 being inducedSubgraph of G,X holds b1 is Component-like
proof
let G2 be inducedSubgraph of G,X; ::_thesis: G2 is Component-like
 ex v being Vertex of G st X = G .reachableFrom v by Def8;
hence  G2 is Component-like ; ::_thesis: verum
end;
end;

definition
let G be _Graph;
funcG .numComponents()  ->  Cardinal equals :: GLIB_002:def 9
 card (G .componentSet());
coherence
 card (G .componentSet()) is Cardinal ;
end;

:: deftheorem  defines .numComponents() GLIB_002:def_9_:_
 for G being _Graph holds G .numComponents() = card (G .componentSet());

definition
let G be finite _Graph;
:: original: .numComponents()
redefine funcG .numComponents()  ->  non empty Element of NAT ;
coherence
 G .numComponents() is non empty Element of NAT
proof
 G .numComponents() = card (G .componentSet()) ;
hence  G .numComponents() is non empty Element of NAT ; ::_thesis: verum
end;
end;

definition
let G be _Graph;
let v be Vertex of G;
attrv is cut-vertex  means :Def10: :: GLIB_002:def 10
 for G2 being removeVertex of G,v holds G .numComponents() in G2 .numComponents() ;
end;

:: deftheorem Def10 defines cut-vertex GLIB_002:def_10_:_
 for G being _Graph
for v being Vertex of G holds
( v is cut-vertex iff for G2 being removeVertex of G,v holds G .numComponents() in G2 .numComponents() );

definition
let G be finite _Graph;
let v be Vertex of G;
redefine attr v is cut-vertex  means :Def11: :: GLIB_002:def 11
 for G2 being removeVertex of G,v holds G .numComponents() < G2 .numComponents() ;
compatibility
 ( v is cut-vertex iff for G2 being removeVertex of G,v holds G .numComponents() < G2 .numComponents() )
proof
hereby  ::_thesis: ( ( for G2 being removeVertex of G,v holds G .numComponents() < G2 .numComponents() ) implies v is cut-vertex )
assume A1: v is cut-vertex ; ::_thesis: for G2 being removeVertex of G,v holds G .numComponents() < G2 .numComponents()
let G2 be removeVertex of G,v; ::_thesis: G .numComponents() < G2 .numComponents()
 card (G .numComponents()) in card (G2 .numComponents()) by A1, Def10;
hence  G .numComponents() < G2 .numComponents() by NAT_1:41; ::_thesis: verum
end;
assume A2: for G2 being removeVertex of G,v holds G .numComponents() < G2 .numComponents() ; ::_thesis: v is cut-vertex
now__::_thesis:_for_G2_being_removeVertex_of_G,v_holds_G_.numComponents()_in_G2_.numComponents()
let G2 be removeVertex of G,v; ::_thesis: G .numComponents() in G2 .numComponents()
 G .numComponents() < G2 .numComponents() by A2;
then  card (G .numComponents()) in card (G2 .numComponents()) by NAT_1:41;
hence  G .numComponents() in G2 .numComponents() ; ::_thesis: verum
end;
hence  v is cut-vertex by Def10; ::_thesis: verum
end;
end;

:: deftheorem Def11 defines cut-vertex GLIB_002:def_11_:_
 for G being finite _Graph
for v being Vertex of G holds
( v is cut-vertex iff for G2 being removeVertex of G,v holds G .numComponents() < G2 .numComponents() );

Lm5:  for G1 being non trivial connected _Graph
for v being Vertex of G1
for G2 being removeVertex of G1,v st v is endvertex holds
G2 is connected
proof
let G1 be non trivial connected _Graph; ::_thesis: for v being Vertex of G1
for G2 being removeVertex of G1,v st v is endvertex holds
G2 is connected
let v be Vertex of G1; ::_thesis: for G2 being removeVertex of G1,v st v is endvertex holds
G2 is connected
let G2 be removeVertex of G1,v; ::_thesis: ( v is endvertex implies G2 is connected )
set VG = the_Vertices_of G1;
set VG2 = the_Vertices_of G2;
assume A1: v is endvertex ; ::_thesis: G2 is connected
then consider ev being set  such that
A2: v .edgesInOut() = {ev} and
 not ev Joins v,v,G1 by GLIB_000:def_51;
now__::_thesis:_for_v19,_v29_being_Vertex_of_G2_ex_W_being_Walk_of_G2_st_W_is_Walk_from_v19,v29
let v19, v29 be Vertex of G2; ::_thesis: ex W being Walk of G2 st W is_Walk_from v19,v29
reconsider v1 = v19, v2 = v29 as Vertex of G1 by GLIB_000:42;
consider W being Walk of G1 such that
A3: W is_Walk_from v1,v2 by Def1;
set T = the Trail of W;
A4: the Trail of W is_Walk_from v1,v2 by A3, GLIB_001:160;
then A5: the Trail of W . (len the Trail of W) = v2 by GLIB_001:17;
 v19 in the_Vertices_of G2 ;
then  v19 in (the_Vertices_of G1) \ {v} by GLIB_000:47;
then A6: not v1 in {v} by XBOOLE_0:def_5;
 v29 in the_Vertices_of G2 ;
then  v29 in (the_Vertices_of G1) \ {v} by GLIB_000:47;
then  not v2 in {v} by XBOOLE_0:def_5;
then A7: v2 <> v by TARSKI:def_1;
A8: the Trail of W . 1 = v1 by A4, GLIB_001:17;
now__::_thesis:_for_e_being_set_st_e_in_the_Trail_of_W_.edges()_holds_
e_in_the_Edges_of_G2
let e be set ; ::_thesis: ( e in the Trail of W .edges() implies e in the_Edges_of G2 )
assume A9: e in the Trail of W .edges() ; ::_thesis: e in the_Edges_of G2
then consider n being even Element of NAT  such that
A10: 1 <= n and
A11: n <= len the Trail of W and
A12: the Trail of W . n = e by GLIB_001:99;
 n in dom the Trail of W by A10, A11, FINSEQ_3:25;
then consider n1 being odd Element of NAT  such that
A13: n1 = n - 1 and
A14: n - 1 in dom the Trail of W and
A15: n + 1 in dom the Trail of W and
A16: the Trail of W . n Joins the Trail of W . n1, the Trail of W . (n + 1),G1 by GLIB_001:9;
A17: n + 1 <= len the Trail of W by A15, FINSEQ_3:25;
A18: n1 <= len the Trail of W by A13, A14, FINSEQ_3:25;
now__::_thesis:_not_e_in_v_.edgesInOut()
assume A19: e in v .edgesInOut() ; ::_thesis: contradiction
then A20: e = ev by A2, TARSKI:def_1;
now__::_thesis:_contradiction
percases ( the Trail of W . n1 = v or the Trail of W . (n + 1) = v ) by A12, A16, A19, GLIB_000:65;
supposeA21: the Trail of W . n1 = v ; ::_thesis: contradiction
reconsider n2 = n1 - 1 as even Element of NAT by ABIAN:12, INT_1:5;
A22: 1 <= n1 by ABIAN:12;
 n1 <> 1 by A6, A8, A21, TARSKI:def_1;
then A23: 1 < n1 by A22, XXREAL_0:1;
then  1 + 1 <= n1 by NAT_1:13;
then A24: (1 + 1) - 1 <= n2 by XREAL_1:13;
 the Trail of W .vertexAt n1 = v by A18, A21, GLIB_001:def_8;
then  the Trail of W . n2 in v .edgesInOut() by A18, A23, GLIB_001:11;
then A25: the Trail of W . n = the Trail of W . n2 by A2, A12, A20, TARSKI:def_1;
 n - 1 < n - 0 by XREAL_1:15;
then  n1 - 1 < n - 0 by A13, XREAL_1:14;
hence  contradiction by A11, A25, A24, GLIB_001:138; ::_thesis: verum
end;
supposeA26: the Trail of W . (n + 1) = v ; ::_thesis: contradiction
then A27: n + 1 < len the Trail of W by A7, A5, A17, XXREAL_0:1;
 the Trail of W .vertexAt (n + 1) = v by A17, A26, GLIB_001:def_8;
then  the Trail of W . ((n + 1) + 1) in v .edgesInOut() by A27, GLIB_001:10;
then A28: the Trail of W . n = the Trail of W . ((n + 1) + 1) by A2, A12, A20, TARSKI:def_1;
 ( n + 0 < n + (1 + 1) & (n + 1) + 1 <= len the Trail of W ) by A27, NAT_1:13, XREAL_1:8;
hence  contradiction by A10, A28, GLIB_001:138; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
then  e in (the_Edges_of G1) \ (v .edgesInOut()) by A9, XBOOLE_0:def_5;
then  e in (the_Edges_of G1) \ (G1 .edgesInOut {v}) by GLIB_000:def_40;
then  e in G1 .edgesBetween ((the_Vertices_of G1) \ {v}) by GLIB_000:35;
hence  e in the_Edges_of G2 by GLIB_000:47; ::_thesis: verum
end;
then A29: the Trail of W .edges() c= the_Edges_of G2 by TARSKI:def_3;
A30: v1 <> v by A6, TARSKI:def_1;
now__::_thesis:_for_x_being_set_st_x_in_the_Trail_of_W_.vertices()_holds_
x_in_the_Vertices_of_G2
let x be set ; ::_thesis: ( x in the Trail of W .vertices() implies x in the_Vertices_of G2 )
assume A31: x in the Trail of W .vertices() ; ::_thesis: x in the_Vertices_of G2
now__::_thesis:_not_x_=_v
assume  x = v ; ::_thesis: contradiction
then  ( v = the Trail of W .first() or v = the Trail of W .last() ) by A1, A31, GLIB_001:143;
hence  contradiction by A30, A7, A4, GLIB_001:def_23; ::_thesis: verum
end;
then  not x in {v} by TARSKI:def_1;
then  x in (the_Vertices_of G1) \ {v} by A31, XBOOLE_0:def_5;
hence  x in the_Vertices_of G2 by GLIB_000:47; ::_thesis: verum
end;
then  the Trail of W .vertices() c= the_Vertices_of G2 by TARSKI:def_3;
then reconsider W9 = the Trail of W as Walk of G2 by A29, GLIB_001:170;
 W9 is_Walk_from v19,v29 by A4, GLIB_001:19;
hence  ex W being Walk of G2 st W is_Walk_from v19,v29 ; ::_thesis: verum
end;
hence  G2 is connected by Def1; ::_thesis: verum
end;

Lm6:  for G being _Graph st ex v1 being Vertex of G st
for v2 being Vertex of G ex W being Walk of G st W is_Walk_from v1,v2 holds
G is connected
proof
let G be _Graph; ::_thesis: ( ex v1 being Vertex of G st
for v2 being Vertex of G ex W being Walk of G st W is_Walk_from v1,v2 implies G is connected )
given v1 being Vertex of G such that A1: for v2 being Vertex of G ex W being Walk of G st W is_Walk_from v1,v2 ; ::_thesis: G is connected
now__::_thesis:_for_x,_y_being_Vertex_of_G_ex_W_being_Walk_of_G_st_W_is_Walk_from_x,y
let x, y be Vertex of G; ::_thesis: ex W being Walk of G st W is_Walk_from x,y
consider W1 being Walk of G such that
A2: W1 is_Walk_from v1,x by A1;
consider W2 being Walk of G such that
A3: W2 is_Walk_from v1,y by A1;
 W1 .reverse() is_Walk_from x,v1 by A2, GLIB_001:23;
then  (W1 .reverse()) .append W2 is_Walk_from x,y by A3, GLIB_001:31;
hence  ex W being Walk of G st W is_Walk_from x,y ; ::_thesis: verum
end;
hence  G is connected by Def1; ::_thesis: verum
end;

Lm7:  for G being _Graph st ex v being Vertex of G st G .reachableFrom v = the_Vertices_of G holds
G is connected
proof
let G be _Graph; ::_thesis: ( ex v being Vertex of G st G .reachableFrom v = the_Vertices_of G implies G is connected )
assume  ex v being Vertex of G st G .reachableFrom v = the_Vertices_of G ; ::_thesis: G is connected
then consider v being Vertex of G such that
A1: G .reachableFrom v = the_Vertices_of G ;
now__::_thesis:_for_x,_y_being_Vertex_of_G_ex_W_being_Walk_of_G_st_W_is_Walk_from_x,y
let x, y be Vertex of G; ::_thesis: ex W being Walk of G st W is_Walk_from x,y
consider W1 being Walk of G such that
A2: W1 is_Walk_from v,x by A1, Def5;
consider W2 being Walk of G such that
A3: W2 is_Walk_from v,y by A1, Def5;
 W1 .reverse() is_Walk_from x,v by A2, GLIB_001:23;
then  (W1 .reverse()) .append W2 is_Walk_from x,y by A3, GLIB_001:31;
hence  ex W being Walk of G st W is_Walk_from x,y ; ::_thesis: verum
end;
hence  G is connected by Def1; ::_thesis: verum
end;

Lm8:  for G being _Graph st G is connected holds
for v being Vertex of G holds G .reachableFrom v = the_Vertices_of G
proof
let G be _Graph; ::_thesis: ( G is connected implies for v being Vertex of G holds G .reachableFrom v = the_Vertices_of G )
assume A1: G is connected ; ::_thesis: for v being Vertex of G holds G .reachableFrom v = the_Vertices_of G
let v be Vertex of G; ::_thesis: G .reachableFrom v = the_Vertices_of G
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_G_.reachableFrom_v_implies_x_in_the_Vertices_of_G_)_&_(_x_in_the_Vertices_of_G_implies_x_in_G_.reachableFrom_v_)_)
let x be set ; ::_thesis: ( ( x in G .reachableFrom v implies x in the_Vertices_of G ) & ( x in the_Vertices_of G implies x in G .reachableFrom v ) )
thus  ( x in G .reachableFrom v implies x in the_Vertices_of G ) ; ::_thesis: ( x in the_Vertices_of G implies x in G .reachableFrom v )
assume  x in the_Vertices_of G ; ::_thesis: x in G .reachableFrom v
then  ex W being Walk of G st W is_Walk_from v,x by A1, Def1;
hence  x in G .reachableFrom v by Def5; ::_thesis: verum
end;
hence  G .reachableFrom v = the_Vertices_of G by TARSKI:1; ::_thesis: verum
end;

Lm9:  for G1, G2 being _Graph
for v1 being Vertex of G1
for v2 being Vertex of G2 st G1 == G2 & v1 = v2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2
proof
let G1, G2 be _Graph; ::_thesis: for v1 being Vertex of G1
for v2 being Vertex of G2 st G1 == G2 & v1 = v2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2
let v1 be Vertex of G1; ::_thesis: for v2 being Vertex of G2 st G1 == G2 & v1 = v2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2
let v2 be Vertex of G2; ::_thesis: ( G1 == G2 & v1 = v2 implies G1 .reachableFrom v1 = G2 .reachableFrom v2 )
assume that
A1: G1 == G2 and
A2: v1 = v2 ; ::_thesis: G1 .reachableFrom v1 = G2 .reachableFrom v2
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_G1_.reachableFrom_v1_implies_x_in_G2_.reachableFrom_v2_)_&_(_x_in_G2_.reachableFrom_v2_implies_x_in_G1_.reachableFrom_v1_)_)
let x be set ; ::_thesis: ( ( x in G1 .reachableFrom v1 implies x in G2 .reachableFrom v2 ) & ( x in G2 .reachableFrom v2 implies x in G1 .reachableFrom v1 ) )
hereby  ::_thesis: ( x in G2 .reachableFrom v2 implies x in G1 .reachableFrom v1 )
assume  x in G1 .reachableFrom v1 ; ::_thesis: x in G2 .reachableFrom v2
then consider W being Walk of G1 such that
A3: W is_Walk_from v2,x by A2, Def5;
reconsider W2 = W as Walk of G2 by A1, GLIB_001:179;
 W2 is_Walk_from v2,x by A3, GLIB_001:19;
hence  x in G2 .reachableFrom v2 by Def5; ::_thesis: verum
end;
assume  x in G2 .reachableFrom v2 ; ::_thesis: x in G1 .reachableFrom v1
then consider W being Walk of G2 such that
A4: W is_Walk_from v1,x by A2, Def5;
reconsider W2 = W as Walk of G1 by A1, GLIB_001:179;
 W2 is_Walk_from v1,x by A4, GLIB_001:19;
hence  x in G1 .reachableFrom v1 by Def5; ::_thesis: verum
end;
hence  G1 .reachableFrom v1 = G2 .reachableFrom v2 by TARSKI:1; ::_thesis: verum
end;

Lm10:  for G1 being _Graph
for G2 being connected Subgraph of G1 st G2 is spanning holds
G1 is connected
proof
let G1 be _Graph; ::_thesis: for G2 being connected Subgraph of G1 st G2 is spanning holds
G1 is connected
let G2 be connected Subgraph of G1; ::_thesis: ( G2 is spanning implies G1 is connected )
assume A1: G2 is spanning ; ::_thesis: G1 is connected
now__::_thesis:_for_u9,_v9_being_Vertex_of_G1_ex_W_being_Walk_of_G1_st_W_is_Walk_from_u9,v9
let u9, v9 be Vertex of G1; ::_thesis: ex W being Walk of G1 st W is_Walk_from u9,v9
reconsider u = u9, v = v9 as Vertex of G2 by A1, GLIB_000:def_33;
consider W being Walk of G2 such that
A2: W is_Walk_from u,v by Def1;
reconsider W = W as Walk of G1 by GLIB_001:167;
take W = W; ::_thesis: W is_Walk_from u9,v9
thus  W is_Walk_from u9,v9 by A2, GLIB_001:19; ::_thesis: verum
end;
hence  G1 is connected by Def1; ::_thesis: verum
end;

Lm11:  for G being _Graph holds
( G is connected iff G .componentSet() = {(the_Vertices_of G)} )
proof
let G be _Graph; ::_thesis: ( G is connected iff G .componentSet() = {(the_Vertices_of G)} )
hereby  ::_thesis: ( G .componentSet() = {(the_Vertices_of G)} implies G is connected )
assume A1: G is connected ; ::_thesis: G .componentSet() = {(the_Vertices_of G)}
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_G_.componentSet()_implies_x_in_{(the_Vertices_of_G)}_)_&_(_x_in_{(the_Vertices_of_G)}_implies_x_in_G_.componentSet()_)_)
set v = the Vertex of G;
let x be set ; ::_thesis: ( ( x in G .componentSet() implies x in {(the_Vertices_of G)} ) & ( x in {(the_Vertices_of G)} implies x in G .componentSet() ) )
hereby  ::_thesis: ( x in {(the_Vertices_of G)} implies x in G .componentSet() )
assume  x in G .componentSet() ; ::_thesis: x in {(the_Vertices_of G)}
then  ex v being Vertex of G st x = G .reachableFrom v by Def8;
then  x = the_Vertices_of G by A1, Lm8;
hence  x in {(the_Vertices_of G)} by TARSKI:def_1; ::_thesis: verum
end;
assume  x in {(the_Vertices_of G)} ; ::_thesis: x in G .componentSet()
then A2: x = the_Vertices_of G by TARSKI:def_1;
 G .reachableFrom the Vertex of G = the_Vertices_of G by A1, Lm8;
hence  x in G .componentSet() by A2, Def8; ::_thesis: verum
end;
hence  G .componentSet() = {(the_Vertices_of G)} by TARSKI:1; ::_thesis: verum
end;
assume  G .componentSet() = {(the_Vertices_of G)} ; ::_thesis: G is connected
then  the_Vertices_of G in G .componentSet() by TARSKI:def_1;
then  ex v being Vertex of G st G .reachableFrom v = the_Vertices_of G by Def8;
hence  G is connected by Lm7; ::_thesis: verum
end;

Lm12:  for G1, G2 being _Graph st G1 == G2 holds
G1 .componentSet() = G2 .componentSet()
proof
let G1, G2 be _Graph; ::_thesis: ( G1 == G2 implies G1 .componentSet() = G2 .componentSet() )
assume A1: G1 == G2 ; ::_thesis: G1 .componentSet() = G2 .componentSet()
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_G1_.componentSet()_implies_x_in_G2_.componentSet()_)_&_(_x_in_G2_.componentSet()_implies_x_in_G1_.componentSet()_)_)
let x be set ; ::_thesis: ( ( x in G1 .componentSet() implies x in G2 .componentSet() ) & ( x in G2 .componentSet() implies x in G1 .componentSet() ) )
hereby  ::_thesis: ( x in G2 .componentSet() implies x in G1 .componentSet() )
assume  x in G1 .componentSet() ; ::_thesis: x in G2 .componentSet()
then consider v1 being Vertex of G1 such that
A2: x = G1 .reachableFrom v1 by Def8;
reconsider v2 = v1 as Vertex of G2 by A1, GLIB_000:def_34;
 x = G2 .reachableFrom v2 by A1, A2, Lm9;
hence  x in G2 .componentSet() by Def8; ::_thesis: verum
end;
assume  x in G2 .componentSet() ; ::_thesis: x in G1 .componentSet()
then consider v2 being Vertex of G2 such that
A3: x = G2 .reachableFrom v2 by Def8;
reconsider v1 = v2 as Vertex of G1 by A1, GLIB_000:def_34;
 x = G1 .reachableFrom v1 by A1, A3, Lm9;
hence  x in G1 .componentSet() by Def8; ::_thesis: verum
end;
hence  G1 .componentSet() = G2 .componentSet() by TARSKI:1; ::_thesis: verum
end;

Lm13:  for G being _Graph
for x being set st x in G .componentSet() holds
x is non empty Subset of (the_Vertices_of G)
proof
let G be _Graph; ::_thesis: for x being set st x in G .componentSet() holds
x is non empty Subset of (the_Vertices_of G)
let x be set ; ::_thesis: ( x in G .componentSet() implies x is non empty Subset of (the_Vertices_of G) )
assume  x in G .componentSet() ; ::_thesis: x is non empty Subset of (the_Vertices_of G)
then  ex v being Vertex of G st x = G .reachableFrom v by Def8;
hence  x is non empty Subset of (the_Vertices_of G) ; ::_thesis: verum
end;

Lm14:  for G being _Graph
for C being Component of G holds the_Edges_of C = G .edgesBetween (the_Vertices_of C)
proof
let G be _Graph; ::_thesis: for C being Component of G holds the_Edges_of C = G .edgesBetween (the_Vertices_of C)
let C be Component of G; ::_thesis: the_Edges_of C = G .edgesBetween (the_Vertices_of C)
reconsider VC = the_Vertices_of C as Subset of (the_Vertices_of G) ;
set EB = G .edgesBetween VC;
 C .edgesBetween (the_Vertices_of C) c= G .edgesBetween VC by GLIB_000:76;
then A1: the_Edges_of C c= G .edgesBetween VC by GLIB_000:34;
now__::_thesis:_for_e_being_set_holds_
(_(_e_in_the_Edges_of_C_implies_e_in_G_.edgesBetween_VC_)_&_(_e_in_G_.edgesBetween_VC_implies_e_in_the_Edges_of_C_)_)
let e be set ; ::_thesis: ( ( e in the_Edges_of C implies e in G .edgesBetween VC ) & ( e in G .edgesBetween VC implies e in the_Edges_of C ) )
thus  ( e in the_Edges_of C implies e in G .edgesBetween VC ) by A1; ::_thesis: ( e in G .edgesBetween VC implies e in the_Edges_of C )
assume A2: e in G .edgesBetween VC ; ::_thesis: e in the_Edges_of C
now__::_thesis:_e_in_the_Edges_of_C
set GX = the inducedSubgraph of G,VC,G .edgesBetween VC;
assume A3: not e in the_Edges_of C ; ::_thesis: contradiction
A4: the_Edges_of the inducedSubgraph of G,VC,G .edgesBetween VC = G .edgesBetween VC by GLIB_000:def_37;
 the_Vertices_of the inducedSubgraph of G,VC,G .edgesBetween VC = VC by GLIB_000:def_37;
then A5: C is spanning Subgraph of the inducedSubgraph of G,VC,G .edgesBetween VC by A1, A4, GLIB_000:44, GLIB_000:def_33;
then  the inducedSubgraph of G,VC,G .edgesBetween VC is connected by Lm10;
then  not C c< the inducedSubgraph of G,VC,G .edgesBetween VC by Def7;
then  ( the inducedSubgraph of G,VC,G .edgesBetween VC == C or not C c= the inducedSubgraph of G,VC,G .edgesBetween VC ) by GLIB_000:def_36;
hence  contradiction by A2, A3, A4, A5, GLIB_000:def_34, GLIB_000:def_35; ::_thesis: verum
end;
hence  e in the_Edges_of C ; ::_thesis: verum
end;
hence  the_Edges_of C = G .edgesBetween (the_Vertices_of C) by TARSKI:1; ::_thesis: verum
end;

Lm15:  for G being _Graph
for C1, C2 being Component of G holds
( the_Vertices_of C1 = the_Vertices_of C2 iff C1 == C2 )
proof
let G be _Graph; ::_thesis: for C1, C2 being Component of G holds
( the_Vertices_of C1 = the_Vertices_of C2 iff C1 == C2 )
let C1, C2 be Component of G; ::_thesis: ( the_Vertices_of C1 = the_Vertices_of C2 iff C1 == C2 )
hereby  ::_thesis: ( C1 == C2 implies the_Vertices_of C1 = the_Vertices_of C2 )
assume A1: the_Vertices_of C1 = the_Vertices_of C2 ; ::_thesis: C1 == C2
then  the_Edges_of C1 = G .edgesBetween (the_Vertices_of C2) by Lm14
.= the_Edges_of C2 by Lm14 ;
hence  C1 == C2 by A1, GLIB_000:86; ::_thesis: verum
end;
assume  C1 == C2 ; ::_thesis: the_Vertices_of C1 = the_Vertices_of C2
hence  the_Vertices_of C1 = the_Vertices_of C2 by GLIB_000:def_34; ::_thesis: verum
end;

Lm16:  for G being _Graph
for C being Component of G
for v being Vertex of G holds
( v in the_Vertices_of C iff the_Vertices_of C = G .reachableFrom v )
proof
let G be _Graph; ::_thesis: for C being Component of G
for v being Vertex of G holds
( v in the_Vertices_of C iff the_Vertices_of C = G .reachableFrom v )
let C be Component of G; ::_thesis: for v being Vertex of G holds
( v in the_Vertices_of C iff the_Vertices_of C = G .reachableFrom v )
let v be Vertex of G; ::_thesis: ( v in the_Vertices_of C iff the_Vertices_of C = G .reachableFrom v )
hereby  ::_thesis: ( the_Vertices_of C = G .reachableFrom v implies v in the_Vertices_of C )
assume A1: v in the_Vertices_of C ; ::_thesis: the_Vertices_of C = G .reachableFrom v
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_the_Vertices_of_C_implies_x_in_G_.reachableFrom_v_)_&_(_x_in_G_.reachableFrom_v_implies_x_in_the_Vertices_of_C_)_)
let x be set ; ::_thesis: ( ( x in the_Vertices_of C implies x in G .reachableFrom v ) & ( x in G .reachableFrom v implies x in the_Vertices_of C ) )
hereby  ::_thesis: ( x in G .reachableFrom v implies x in the_Vertices_of C )
assume  x in the_Vertices_of C ; ::_thesis: x in G .reachableFrom v
then reconsider x9 = x as Vertex of C ;
consider W being Walk of C such that
A2: W is_Walk_from v,x9 by A1, Def1;
reconsider W = W as Walk of G by GLIB_001:167;
 W is_Walk_from v,x by A2, GLIB_001:19;
hence  x in G .reachableFrom v by Def5; ::_thesis: verum
end;
assume A3: x in G .reachableFrom v ; ::_thesis: x in the_Vertices_of C
then reconsider x9 = x as Vertex of G ;
A4: G .reachableFrom x9 = G .reachableFrom v by A3, Lm3;
set CX = the inducedSubgraph of G,(G .reachableFrom x9);
 not C c< the inducedSubgraph of G,(G .reachableFrom x9) by Def7;
then A5: ( C == the inducedSubgraph of G,(G .reachableFrom x9) or not C c= the inducedSubgraph of G,(G .reachableFrom x9) ) by GLIB_000:def_36;
A6: the_Edges_of the inducedSubgraph of G,(G .reachableFrom x9) = G .edgesBetween (G .reachableFrom x9) by GLIB_000:def_37;
now__::_thesis:_for_e_being_set_st_e_in_the_Edges_of_C_holds_
e_in_the_Edges_of_the_inducedSubgraph_of_G,(G_.reachableFrom_x9)
let e be set ; ::_thesis: ( e in the_Edges_of C implies e in the_Edges_of the inducedSubgraph of G,(G .reachableFrom x9) )
set v1 = (the_Source_of C) . e;
set v2 = (the_Target_of C) . e;
assume A7: e in the_Edges_of C ; ::_thesis: e in the_Edges_of the inducedSubgraph of G,(G .reachableFrom x9)
then reconsider v1 = (the_Source_of C) . e, v2 = (the_Target_of C) . e as Vertex of C by FUNCT_2:5;
 e Joins v1,v2,C by A7, GLIB_000:def_13;
then A8: e Joins v1,v2,G by GLIB_000:72;
consider W1 being Walk of C such that
A9: W1 is_Walk_from v,v1 by A1, Def1;
reconsider W1 = W1 as Walk of G by GLIB_001:167;
consider W2 being Walk of C such that
A10: W2 is_Walk_from v,v2 by A1, Def1;
reconsider W2 = W2 as Walk of G by GLIB_001:167;
 W2 is_Walk_from v,v2 by A10, GLIB_001:19;
then A11: v2 in G .reachableFrom x9 by A4, Def5;
 W1 is_Walk_from v,v1 by A9, GLIB_001:19;
then  v1 in G .reachableFrom x9 by A4, Def5;
hence  e in the_Edges_of the inducedSubgraph of G,(G .reachableFrom x9) by A6, A8, A11, GLIB_000:32; ::_thesis: verum
end;
then A12: the_Edges_of C c= the_Edges_of the inducedSubgraph of G,(G .reachableFrom x9) by TARSKI:def_3;
A13: the_Vertices_of the inducedSubgraph of G,(G .reachableFrom x9) = G .reachableFrom x9 by GLIB_000:def_37;
now__::_thesis:_for_z_being_set_st_z_in_the_Vertices_of_C_holds_
z_in_the_Vertices_of_the_inducedSubgraph_of_G,(G_.reachableFrom_x9)
let z be set ; ::_thesis: ( z in the_Vertices_of C implies z in the_Vertices_of the inducedSubgraph of G,(G .reachableFrom x9) )
assume  z in the_Vertices_of C ; ::_thesis: z in the_Vertices_of the inducedSubgraph of G,(G .reachableFrom x9)
then consider W being Walk of C such that
A14: W is_Walk_from v,z by A1, Def1;
reconsider W = W as Walk of G by GLIB_001:167;
 W is_Walk_from v,z by A14, GLIB_001:19;
hence  z in the_Vertices_of the inducedSubgraph of G,(G .reachableFrom x9) by A13, A4, Def5; ::_thesis: verum
end;
then  the_Vertices_of C c= the_Vertices_of the inducedSubgraph of G,(G .reachableFrom x9) by TARSKI:def_3;
then A15: C is Subgraph of the inducedSubgraph of G,(G .reachableFrom x9) by A12, GLIB_000:44;
 x in the_Vertices_of the inducedSubgraph of G,(G .reachableFrom x9) by A13, Lm1;
hence  x in the_Vertices_of C by A5, A15, GLIB_000:def_34, GLIB_000:def_35; ::_thesis: verum
end;
hence  the_Vertices_of C = G .reachableFrom v by TARSKI:1; ::_thesis: verum
end;
assume  the_Vertices_of C = G .reachableFrom v ; ::_thesis: v in the_Vertices_of C
hence  v in the_Vertices_of C by Lm1; ::_thesis: verum
end;

Lm17:  for G being _Graph
for C1, C2 being Component of G
for v being set st v in the_Vertices_of C1 & v in the_Vertices_of C2 holds
C1 == C2
proof
let G be _Graph; ::_thesis: for C1, C2 being Component of G
for v being set st v in the_Vertices_of C1 & v in the_Vertices_of C2 holds
C1 == C2
let C1, C2 be Component of G; ::_thesis: for v being set st v in the_Vertices_of C1 & v in the_Vertices_of C2 holds
C1 == C2
let v be set ; ::_thesis: ( v in the_Vertices_of C1 & v in the_Vertices_of C2 implies C1 == C2 )
assume that
A1: v in the_Vertices_of C1 and
A2: v in the_Vertices_of C2 ; ::_thesis: C1 == C2
reconsider v9 = v as Vertex of G by A1;
 ( the_Vertices_of C1 = G .reachableFrom v9 & the_Vertices_of C2 = G .reachableFrom v9 ) by A1, A2, Lm16;
hence  C1 == C2 by Lm15; ::_thesis: verum
end;

Lm18:  for G being _Graph holds
( G is connected iff G .numComponents() = 1 )
proof
let G be _Graph; ::_thesis: ( G is connected iff G .numComponents() = 1 )
hereby  ::_thesis: ( G .numComponents() = 1 implies G is connected )
assume  G is connected ; ::_thesis: G .numComponents() = 1
then  G .componentSet() = {(the_Vertices_of G)} by Lm11;
hence  G .numComponents() = 1 by CARD_1:30; ::_thesis: verum
end;
assume  G .numComponents() = 1 ; ::_thesis: G is connected
then consider V being set  such that
A1: G .componentSet() = {V} by CARD_2:42;
now__::_thesis:_for_v_being_set_st_v_in_the_Vertices_of_G_holds_
v_in_V
let v be set ; ::_thesis: ( v in the_Vertices_of G implies v in V )
assume  v in the_Vertices_of G ; ::_thesis: v in V
then reconsider v9 = v as Vertex of G ;
now__::_thesis:_v_in_V
set V2 = G .reachableFrom v9;
assume A2: not v in V ; ::_thesis: contradiction
 G .reachableFrom v9 in G .componentSet() by Def8;
then  not v in G .reachableFrom v9 by A1, A2, TARSKI:def_1;
hence  contradiction by Lm1; ::_thesis: verum
end;
hence  v in V ; ::_thesis: verum
end;
then A3: the_Vertices_of G c= V by TARSKI:def_3;
 V in G .componentSet() by A1, TARSKI:def_1;
then  V = the_Vertices_of G by A3, XBOOLE_0:def_10;
hence  G is connected by A1, Lm11; ::_thesis: verum
end;

Lm19:  for G being connected _Graph
for v being Vertex of G holds
( not v is cut-vertex iff for G2 being removeVertex of G,v holds G2 .numComponents() c= G .numComponents() )
proof
let G be connected _Graph; ::_thesis: for v being Vertex of G holds
( not v is cut-vertex iff for G2 being removeVertex of G,v holds G2 .numComponents() c= G .numComponents() )
let v be Vertex of G; ::_thesis: ( not v is cut-vertex iff for G2 being removeVertex of G,v holds G2 .numComponents() c= G .numComponents() )
hereby  ::_thesis: ( ( for G2 being removeVertex of G,v holds G2 .numComponents() c= G .numComponents() ) implies not v is cut-vertex )
assume  not v is cut-vertex ; ::_thesis: for G2 being removeVertex of G,v holds G2 .numComponents() c= G .numComponents()
then consider G3 being removeVertex of G,v such that
A1: not G .numComponents() in G3 .numComponents() by Def10;
let G2 be removeVertex of G,v; ::_thesis: G2 .numComponents() c= G .numComponents()
 G3 .numComponents() c= G .numComponents() by A1, CARD_1:4;
hence  G2 .numComponents() c= G .numComponents() by Lm12, GLIB_000:93; ::_thesis: verum
end;
assume A2: for G2 being removeVertex of G,v holds G2 .numComponents() c= G .numComponents() ; ::_thesis: not v is cut-vertex
now__::_thesis:_not__for_G3_being_removeVertex_of_G,v_holds_G_.numComponents()_in_G3_.numComponents()
set X = the removeVertex of G,v;
assume  for G3 being removeVertex of G,v holds G .numComponents() in G3 .numComponents() ; ::_thesis: contradiction
then A3: G .numComponents() in the removeVertex of G,v .numComponents() ;
 the removeVertex of G,v .numComponents() c= G .numComponents() by A2;
hence  contradiction by A3, CARD_1:4; ::_thesis: verum
end;
hence  not v is cut-vertex by Def10; ::_thesis: verum
end;

Lm20:  for G being connected _Graph
for v being Vertex of G
for G2 being removeVertex of G,v st not v is cut-vertex holds
G2 is connected
proof
let G be connected _Graph; ::_thesis: for v being Vertex of G
for G2 being removeVertex of G,v st not v is cut-vertex holds
G2 is connected
let v be Vertex of G; ::_thesis: for G2 being removeVertex of G,v st not v is cut-vertex holds
G2 is connected
let G2 be removeVertex of G,v; ::_thesis: ( not v is cut-vertex implies G2 is connected )
assume A1: not v is cut-vertex ; ::_thesis: G2 is connected
 G .numComponents() = 1 by Lm18;
then  G2 .numComponents() c= succ 0 by A1, Lm19;
then  G2 .numComponents() c= {} \/ {{}} by ORDINAL1:def_1;
then G2 .numComponents() = {} \/ {{}} by ZFMISC_1:33
.= succ 0 by ORDINAL1:def_1
.= 1 ;
hence  G2 is connected by Lm18; ::_thesis: verum
end;

Lm21:  for G being finite non trivial connected _Graph ex v1, v2 being Vertex of G st
( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex )
proof
let G be finite non trivial connected _Graph; ::_thesis: ex v1, v2 being Vertex of G st
( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex )
defpred S1[ Nat] means  for G being finite non trivial connected _Graph st G .order() = $1 holds
ex v1, v2 being Vertex of G st
( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex );
now__::_thesis:_for_k_being_Nat_st_(_for_n_being_Nat_st_n_<_k_holds_
S1[n]_)_holds_
S1[k]
let k be Nat; ::_thesis: ( ( for n being Nat st n < k holds
S1[n] ) implies S1[k] )
assume A1: for n being Nat st n < k holds
S1[n] ; ::_thesis: S1[k]
now__::_thesis:_for_G_being_finite_non_trivial_connected__Graph_st_G_.order()_=_k_holds_
ex_v1,_v2_being_Vertex_of_G_st_
(_v1_<>_v2_&_not_v1_is_cut-vertex_&_not_v2_is_cut-vertex_)
let G be finite non trivial connected _Graph; ::_thesis: ( G .order() = k implies ex v1, v2 being Vertex of G st
( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex ) )
assume A2: G .order() = k ; ::_thesis: ex v1, v2 being Vertex of G st
( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex )
A3: G .numComponents() = 1 by Lm18;
now__::_thesis:_ex_v1,_v2_being_Vertex_of_G_st_
(_v1_<>_v2_&_not_v1_is_cut-vertex_&_not_v2_is_cut-vertex_)
percases ( for v being Vertex of G holds not v is cut-vertex or ex cv being Vertex of G st cv is cut-vertex ) ;
supposeA4: for v being Vertex of G holds not v is cut-vertex ; ::_thesis: ex v1, v2 being Vertex of G st
( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex )
consider v1, v2 being Vertex of G such that
A5: v1 <> v2 by GLIB_000:21;
take v1 = v1; ::_thesis: ex v2 being Vertex of G st
( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex )
take v2 = v2; ::_thesis: ( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex )
thus  v1 <> v2 by A5; ::_thesis: ( not v1 is cut-vertex & not v2 is cut-vertex )
thus  ( not v1 is cut-vertex & not v2 is cut-vertex ) by A4; ::_thesis: verum
end;
suppose ex cv being Vertex of G st cv is cut-vertex ; ::_thesis: ex v1, v2 being Vertex of G st
( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex )
then consider cv being Vertex of G such that
A6: cv is cut-vertex ;
set G2 = the removeVertex of G,cv;
 1 < the removeVertex of G,cv .numComponents() by A3, A6, Def11;
then  1 + 1 <= the removeVertex of G,cv .numComponents() by NAT_1:13;
then  card 2 <= card ( the removeVertex of G,cv .componentSet()) by CARD_1:def_2;
then  card 2 c= card ( the removeVertex of G,cv .componentSet()) by NAT_1:39;
then  2 c= card ( the removeVertex of G,cv .componentSet()) by CARD_1:def_2;
then consider C1, C2 being set  such that
A7: ( C1 in the removeVertex of G,cv .componentSet() & C2 in the removeVertex of G,cv .componentSet() ) and
A8: C1 <> C2 by PENCIL_1:2;
reconsider C1 = C1, C2 = C2 as Element of the removeVertex of G,cv .componentSet() by A7;
set CC1 = the inducedSubgraph of the removeVertex of G,cv,C1;
set CC2 = the inducedSubgraph of the removeVertex of G,cv,C2;
A9: the_Vertices_of the removeVertex of G,cv = (the_Vertices_of G) \ {cv} by GLIB_000:47;
 G .edgesBetween ((the_Vertices_of G) \ {cv}) = (the_Edges_of G) \ (G .edgesInOut {cv}) by GLIB_000:35;
then  G .edgesBetween ((the_Vertices_of G) \ {cv}) = (the_Edges_of G) \ (cv .edgesInOut()) by GLIB_000:def_40;
then A10: the_Edges_of the removeVertex of G,cv = (the_Edges_of G) \ (cv .edgesInOut()) by GLIB_000:47;
A11: ( the removeVertex of G,cv .order()) + 1 = k by A2, GLIB_000:48;
A12: now__::_thesis:_for_C_being_Component_of_the_removeVertex_of_G,cv_ex_v_being_Vertex_of_G_st_
(_v_in_the_Vertices_of_C_&_not_v_is_cut-vertex_)
let C be Component of the removeVertex of G,cv; ::_thesis: ex v being Vertex of G st
( v in the_Vertices_of C & not v is cut-vertex )
now__::_thesis:_ex_a_being_Vertex_of_C_ex_e_being_set_st_e_Joins_cv,a,G
set x = the Vertex of C;
assume A13: for a being Vertex of C
for e being set holds not e Joins cv,a,G ; ::_thesis: contradiction
 the_Vertices_of C c= the_Vertices_of the removeVertex of G,cv ;
then reconsider x9 = the Vertex of C as Vertex of the removeVertex of G,cv by TARSKI:def_3;
 the_Vertices_of the removeVertex of G,cv c= the_Vertices_of G ;
then reconsider x99 = x9 as Vertex of G by TARSKI:def_3;
consider W being Walk of G such that
A14: W is_Walk_from cv,x99 by Def1;
set P = the Path of W;
A15: the Path of W is_Walk_from cv,x99 by A14, GLIB_001:160;
then A16: the Path of W .first() = cv by GLIB_001:def_23;
set P2 = the Path of W .cut (((2 * 1) + 1),(len the Path of W));
A17: 1 <= len the Path of W by ABIAN:12;
A18: the Path of W .last() = the Vertex of C by A15, GLIB_001:def_23;
then A19: the Path of W . (len the Path of W) = the Vertex of C by GLIB_001:def_7;
 not x9 in {cv} by A9, XBOOLE_0:def_5;
then A20: the Vertex of C <> cv by TARSKI:def_1;
then A21: not the Path of W is trivial by A16, A18, GLIB_001:127;
then A22: (2 * 1) + 1 <= len the Path of W by GLIB_001:125;
then  the Path of W .cut (((2 * 1) + 1),(len the Path of W)) is_Walk_from the Path of W . 3, the Path of W . (len the Path of W) by GLIB_001:37;
then A23: the Path of W .cut (((2 * 1) + 1),(len the Path of W)) is_Walk_from the Path of W . 3, the Vertex of C by A18, GLIB_001:def_7;
A24: the Path of W . ((2 * 0) + 1) = cv by A16, GLIB_001:def_6;
now__::_thesis:_not_cv_in_(_the_Path_of_W_.cut_(((2_*_1)_+_1),(len_the_Path_of_W)))_.vertices()
assume  cv in ( the Path of W .cut (((2 * 1) + 1),(len the Path of W))) .vertices() ; ::_thesis: contradiction
then consider n being odd Element of NAT  such that
A25: n <= len ( the Path of W .cut (((2 * 1) + 1),(len the Path of W))) and
A26: ( the Path of W .cut (((2 * 1) + 1),(len the Path of W))) . n = cv by GLIB_001:87;
A27: 1 <= n by ABIAN:12;
then A28: 1 + 0 < n + 2 by XREAL_1:8;
A29: n in dom ( the Path of W .cut (((2 * 1) + 1),(len the Path of W))) by A25, A27, FINSEQ_3:25;
then  (3 + n) - 1 in dom the Path of W by A22, GLIB_001:47;
then A30: 2 + n <= len the Path of W by FINSEQ_3:25;
 the Path of W . ((3 + n) - 1) = cv by A22, A26, A29, GLIB_001:47;
hence  contradiction by A20, A24, A19, A30, A28, GLIB_001:def_28; ::_thesis: verum
end;
then reconsider P2 = the Path of W .cut (((2 * 1) + 1),(len the Path of W)) as Walk of the removeVertex of G,cv by GLIB_001:171;
 P2 is_Walk_from the Path of W . 3, the Vertex of C by A23, GLIB_001:19;
then  P2 .reverse() is_Walk_from the Vertex of C, the Path of W . 3 by GLIB_001:23;
then A31: the Path of W . 3 in the removeVertex of G,cv .reachableFrom x9 by Def5;
 len the Path of W <> 1 by A21, GLIB_001:125;
then  (2 * 0) + 1 < len the Path of W by A17, XXREAL_0:1;
then  the Path of W . (1 + 1) Joins the Path of W . 1, the Path of W . (1 + 2),G by GLIB_001:def_3;
then A32: the Path of W . 2 Joins cv, the Path of W . 3,G by A16, GLIB_001:def_6;
 the_Vertices_of C = the removeVertex of G,cv .reachableFrom x9 by Lm16;
hence  contradiction by A13, A32, A31; ::_thesis: verum
end;
then consider a being Vertex of C, e being set  such that
A33: e Joins cv,a,G ;
A34: e in the_Edges_of G by A33, GLIB_000:def_13;
now__::_thesis:_ex_v_being_Vertex_of_G_st_
(_v_in_the_Vertices_of_C_&_not_v_is_cut-vertex_)
percases ( C is trivial or not C is trivial ) ;
suppose C is trivial ; ::_thesis: ex v being Vertex of G st
( v in the_Vertices_of C & not v is cut-vertex )
then consider v99 being Vertex of C such that
A35: the_Vertices_of C = {v99} by GLIB_000:22;
 the_Vertices_of C c= the_Vertices_of the removeVertex of G,cv ;
then reconsider v9 = v99 as Vertex of the removeVertex of G,cv by TARSKI:def_3;
reconsider v = v9 as Vertex of G by GLIB_000:42;
take v = v; ::_thesis: ( v in the_Vertices_of C & not v is cut-vertex )
thus  v in the_Vertices_of C ; ::_thesis: not v is cut-vertex
 not v9 in {cv} by A9, XBOOLE_0:def_5;
then A36: v9 <> cv by TARSKI:def_1;
A37: {v9} = the removeVertex of G,cv .reachableFrom v9 by A35, Lm16;
now__::_thesis:_not_v_is_cut-vertex
set G3 = the removeVertex of G,v;
A38: now__::_thesis:_for_e,_z_being_set_holds_
(_not_e_Joins_v,z,G_or_z_=_v_or_z_=_cv_)
let e, z be set ; ::_thesis: ( not e Joins v,z,G or z = v or z = cv )
assume A39: e Joins v,z,G ; ::_thesis: ( z = v or z = cv )
then A40: e in the_Edges_of G by GLIB_000:def_13;
now__::_thesis:_(_z_<>_v_implies_not_z_<>_cv_)
assume that
A41: z <> v and
A42: z <> cv ; ::_thesis: contradiction
 not e in cv .edgesInOut() by A36, A39, A42, GLIB_000:65;
then  e in the_Edges_of the removeVertex of G,cv by A10, A40, XBOOLE_0:def_5;
then  e Joins v,z, the removeVertex of G,cv by A39, GLIB_000:73;
then  z in the removeVertex of G,cv .reachableFrom v9 by Lm1, Lm2;
hence  contradiction by A37, A41, TARSKI:def_1; ::_thesis: verum
end;
hence  ( z = v or z = cv ) ; ::_thesis: verum
end;
now__::_thesis:_for_x,_y_being_Vertex_of_the_removeVertex_of_G,v_ex_P_being_Walk_of_the_removeVertex_of_G,v_st_P_is_Walk_from_x,y
let x, y be Vertex of the removeVertex of G,v; ::_thesis: ex P being Walk of the removeVertex of G,v st P is_Walk_from x,y
now__::_thesis:_ex_W_being_Walk_of_the_removeVertex_of_G,v_st_W_is_Walk_from_x,y
percases ( x = y or x <> y ) ;
supposeA43: x = y ; ::_thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from x,y
set W = the removeVertex of G,v .walkOf x;
take W = the removeVertex of G,v .walkOf x; ::_thesis: W is_Walk_from x,y
thus  W is_Walk_from x,y by A43, GLIB_001:13; ::_thesis: verum
end;
supposeA44: x <> y ; ::_thesis: ex P being Walk of the removeVertex of G,v st P is_Walk_from x,y
reconsider x9 = x, y9 = y as Vertex of G by GLIB_000:42;
consider W being Walk of G such that
A45: W is_Walk_from x9,y9 by Def1;
set P = the Path of W;
A46: the Path of W is_Walk_from x9,y9 by A45, GLIB_001:160;
A47: the_Vertices_of the removeVertex of G,v = (the_Vertices_of G) \ {v} by GLIB_000:47;
then  not x in {v} by XBOOLE_0:def_5;
then  x <> v by TARSKI:def_1;
then A48: v <> the Path of W . 1 by A46, GLIB_001:17;
 not y in {v} by A47, XBOOLE_0:def_5;
then  y <> v by TARSKI:def_1;
then A49: v <> the Path of W . (len the Path of W) by A46, GLIB_001:17;
now__::_thesis:_not_v_in_the_Path_of_W_.vertices()
assume  v in the Path of W .vertices() ; ::_thesis: contradiction
then consider n being odd Element of NAT  such that
A50: n <= len the Path of W and
A51: the Path of W . n = v by GLIB_001:87;
 1 <= n by ABIAN:12;
then  1 < n by A48, A51, XXREAL_0:1;
then  1 + 1 <= n by NAT_1:13;
then reconsider n2 = n - (2 * 1) as odd Element of NAT by INT_1:5;
A52: now__::_thesis:_not_the_Path_of_W_._n2_=_v
A53: n2 < n - 0 by XREAL_1:15;
assume  the Path of W . n2 = v ; ::_thesis: contradiction
hence  contradiction by A48, A50, A51, A53, GLIB_001:def_28; ::_thesis: verum
end;
set e1 = the Path of W . (n2 + 1);
set e2 = the Path of W . (n + 1);
 n - 2 < (len the Path of W) - 0 by A50, XREAL_1:15;
then  the Path of W . (n2 + 1) Joins the Path of W . n2, the Path of W . (n2 + 2),G by GLIB_001:def_3;
then A54: the Path of W . n2 = cv by A38, A51, A52, GLIB_000:14;
A55: n < len the Path of W by A49, A50, A51, XXREAL_0:1;
then A56: n + 2 <= len the Path of W by GLIB_001:1;
A57: now__::_thesis:_not_the_Path_of_W_._(n_+_2)_=_v
A58: n + 0 < n + 2 by XREAL_1:8;
assume  the Path of W . (n + 2) = v ; ::_thesis: contradiction
hence  contradiction by A48, A51, A56, A58, GLIB_001:def_28; ::_thesis: verum
end;
 n2 < n - 0 by XREAL_1:15;
then A59: n2 + 0 < n + 2 by XREAL_1:8;
 the Path of W . (n + 1) Joins v, the Path of W . (n + 2),G by A51, A55, GLIB_001:def_3;
then A60: the Path of W . (n + 2) = cv by A38, A57;
then  cv = the Path of W . 1 by A54, A56, A59, GLIB_001:def_28;
then A61: cv = x by A46, GLIB_001:17;
 cv = the Path of W . (len the Path of W) by A54, A56, A60, A59, GLIB_001:def_28;
hence  contradiction by A44, A46, A61, GLIB_001:17; ::_thesis: verum
end;
then reconsider P = the Path of W as Walk of the removeVertex of G,v by GLIB_001:171;
take P = P; ::_thesis: P is_Walk_from x,y
thus  P is_Walk_from x,y by A46, GLIB_001:19; ::_thesis: verum
end;
end;
end;
hence  ex P being Walk of the removeVertex of G,v st P is_Walk_from x,y ; ::_thesis: verum
end;
then A62: the removeVertex of G,v is connected by Def1;
assume  v is cut-vertex ; ::_thesis: contradiction
then  1 < the removeVertex of G,v .numComponents() by A3, Def11;
hence  contradiction by A62, Lm18; ::_thesis: verum
end;
hence  not v is cut-vertex ; ::_thesis: verum
end;
suppose not C is trivial ; ::_thesis: ex v being Vertex of G st
( v in the_Vertices_of C & not v is cut-vertex )
then reconsider C9 = C as non trivial _Graph ;
 (C .order()) + 0 < ( the removeVertex of G,cv .order()) + 1 by GLIB_000:75, XREAL_1:8;
then consider v1, v2 being Vertex of C9 such that
A63: v1 <> v2 and
A64: not v1 is cut-vertex and
A65: not v2 is cut-vertex by A1, A11;
set C9R1 = the removeVertex of C9,v1;
A66: the removeVertex of C9,v1 is connected by A64, Lm20;
set C9R2 = the removeVertex of C9,v2;
A67: the_Vertices_of the removeVertex of C9,v1 = (the_Vertices_of C9) \ {v1} by GLIB_000:47;
 v2 in the_Vertices_of the removeVertex of G,cv by GLIB_000:42;
then  not v2 in {cv} by A9, XBOOLE_0:def_5;
then A68: v2 <> cv by TARSKI:def_1;
A69: the_Vertices_of the removeVertex of C9,v2 = (the_Vertices_of C9) \ {v2} by GLIB_000:47;
 v1 in the_Vertices_of the removeVertex of G,cv by GLIB_000:42;
then  not v1 in {cv} by A9, XBOOLE_0:def_5;
then A70: v1 <> cv by TARSKI:def_1;
A71: the removeVertex of C9,v2 is connected by A65, Lm20;
now__::_thesis:_ex_v_being_Vertex_of_G_st_
(_v_in_the_Vertices_of_C_&_not_v_is_cut-vertex_)
percases ( not v1 in cv .allNeighbors() or ( v1 in cv .allNeighbors() & not v2 in cv .allNeighbors() ) or ( v1 in cv .allNeighbors() & v2 in cv .allNeighbors() ) ) ;
supposeA72: not v1 in cv .allNeighbors() ; ::_thesis: ex v being Vertex of G st
( v in the_Vertices_of C & not v is cut-vertex )
reconsider v9 = v1 as Vertex of the removeVertex of G,cv by GLIB_000:42;
reconsider v = v9 as Vertex of G by GLIB_000:42;
take v = v; ::_thesis: ( v in the_Vertices_of C & not v is cut-vertex )
thus  v in the_Vertices_of C ; ::_thesis: not v is cut-vertex
set G3 = the removeVertex of G,v;
A73: the_Vertices_of the removeVertex of G,v = (the_Vertices_of G) \ {v} by GLIB_000:47;
 not cv in {v} by A70, TARSKI:def_1;
then reconsider cv9 = cv as Vertex of the removeVertex of G,v by A73, XBOOLE_0:def_5;
A74: v1 <> a by A33, A72, GLIB_000:71;
A75: the_Vertices_of C = the removeVertex of G,cv .reachableFrom v9 by Lm16;
now__::_thesis:_for_y_being_Vertex_of_the_removeVertex_of_G,v_ex_W_being_Walk_of_the_removeVertex_of_G,v_st_W_is_Walk_from_cv9,y
let y be Vertex of the removeVertex of G,v; ::_thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
now__::_thesis:_ex_W_being_Walk_of_the_removeVertex_of_G,v_st_W_is_Walk_from_cv9,y
percases ( y = cv or y <> cv ) ;
suppose y = cv ; ::_thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
then  the removeVertex of G,v .walkOf y is_Walk_from cv9,y by GLIB_001:13;
hence  ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y ; ::_thesis: verum
end;
supposeA76: y <> cv ; ::_thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
now__::_thesis:_ex_W_being_Walk_of_the_removeVertex_of_G,v_st_W_is_Walk_from_cv9,y
percases ( y in the_Vertices_of C or not y in the_Vertices_of C ) ;
supposeA77: y in the_Vertices_of C ; ::_thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
 not a in {v1} by A74, TARSKI:def_1;
then A78: a in the_Vertices_of the removeVertex of C9,v1 by A67, XBOOLE_0:def_5;
 not y in {v1} by A73, XBOOLE_0:def_5;
then  y in the_Vertices_of the removeVertex of C9,v1 by A67, A77, XBOOLE_0:def_5;
then consider W being Walk of the removeVertex of C9,v1 such that
A79: W is_Walk_from y,a by A66, A78, Def1;
A80: ( W . 1 = y & W . (len W) = a ) by A79, GLIB_001:17;
A81: now__::_thesis:_not_v_in_W_.vertices()
assume  v in W .vertices() ; ::_thesis: contradiction
then  not v in {v1} by A67, XBOOLE_0:def_5;
hence  contradiction by TARSKI:def_1; ::_thesis: verum
end;
 not e in v .edgesInOut() by A33, A70, A74, GLIB_000:65;
then  e in (the_Edges_of G) \ (v .edgesInOut()) by A34, XBOOLE_0:def_5;
then  e in (the_Edges_of G) \ (G .edgesInOut {v}) by GLIB_000:def_40;
then  e in G .edgesBetween ((the_Vertices_of G) \ {v}) by GLIB_000:35;
then  e in the_Edges_of the removeVertex of G,v by GLIB_000:47;
then  e Joins cv,a, the removeVertex of G,v by A33, GLIB_000:73;
then A82: e Joins a,cv, the removeVertex of G,v by GLIB_000:14;
reconsider W = W as Walk of C by GLIB_001:167;
reconsider W = W as Walk of the removeVertex of G,cv by GLIB_001:167;
reconsider W = W as Walk of G by GLIB_001:167;
 not v in W .vertices() by A81, GLIB_001:98;
then reconsider W = W as Walk of the removeVertex of G,v by GLIB_001:171;
 W is_Walk_from y,a by A80, GLIB_001:17;
then  W .addEdge e is_Walk_from y,cv by A82, GLIB_001:66;
then  (W .addEdge e) .reverse() is_Walk_from cv,y by GLIB_001:23;
hence  ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y ; ::_thesis: verum
end;
supposeA83: not y in the_Vertices_of C ; ::_thesis: ex P being Walk of the removeVertex of G,v st P is_Walk_from cv9,y
reconsider y9 = y as Vertex of G by GLIB_000:42;
consider W being Walk of G such that
A84: W is_Walk_from cv,y9 by Def1;
set P = the Path of W;
A85: the Path of W is_Walk_from cv,y9 by A84, GLIB_001:160;
then A86: the Path of W . (len the Path of W) = y9 by GLIB_001:17;
A87: the Path of W . 1 = cv by A85, GLIB_001:17;
now__::_thesis:_not_v_in_the_Path_of_W_.vertices()
assume  v in the Path of W .vertices() ; ::_thesis: contradiction
then consider n being odd Element of NAT  such that
A88: n <= len the Path of W and
A89: the Path of W . n = v by GLIB_001:87;
set P2 = the Path of W .cut (n,(len the Path of W));
A90: the Path of W .cut (n,(len the Path of W)) is_Walk_from v,y9 by A86, A88, A89, GLIB_001:37;
 1 <= n by ABIAN:12;
then A91: 1 < n by A70, A87, A89, XXREAL_0:1;
now__::_thesis:_not_cv_in_(_the_Path_of_W_.cut_(n,(len_the_Path_of_W)))_.vertices()
assume  cv in ( the Path of W .cut (n,(len the Path of W))) .vertices() ; ::_thesis: contradiction
then consider m being odd Element of NAT  such that
A92: m <= len ( the Path of W .cut (n,(len the Path of W))) and
A93: ( the Path of W .cut (n,(len the Path of W))) . m = cv by GLIB_001:87;
 1 <= m by ABIAN:12;
then A94: m in dom ( the Path of W .cut (n,(len the Path of W))) by A92, FINSEQ_3:25;
then A95: the Path of W . ((n + m) - 1) = cv by A88, A93, GLIB_001:47;
 1 + 1 < n + m by A91, ABIAN:12, XREAL_1:8;
then  (1 + 1) - 1 < (n + m) - 1 by XREAL_1:14;
then A96: (2 * 0) + 1 < (n + m) - 1 ;
A97: (n + m) - 1 in dom the Path of W by A88, A94, GLIB_001:47;
then  (n + m) - 1 <= len the Path of W by FINSEQ_3:25;
hence  contradiction by A76, A87, A86, A95, A97, A96, GLIB_001:def_28; ::_thesis: verum
end;
then reconsider P2 = the Path of W .cut (n,(len the Path of W)) as Walk of the removeVertex of G,cv by GLIB_001:171;
 P2 is_Walk_from v,y9 by A90, GLIB_001:19;
hence  contradiction by A75, A83, Def5; ::_thesis: verum
end;
then reconsider P = the Path of W as Walk of the removeVertex of G,v by GLIB_001:171;
take P = P; ::_thesis: P is_Walk_from cv9,y
thus  P is_Walk_from cv9,y by A85, GLIB_001:19; ::_thesis: verum
end;
end;
end;
hence  ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y ; ::_thesis: verum
end;
end;
end;
hence  ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y ; ::_thesis: verum
end;
then  the removeVertex of G,v is connected by Lm6;
then  the removeVertex of G,v .numComponents() = 1 by Lm18;
hence  not v is cut-vertex by A3, Def11; ::_thesis: verum
end;
supposeA98: ( v1 in cv .allNeighbors() & not v2 in cv .allNeighbors() ) ; ::_thesis: ex v being Vertex of G st
( v in the_Vertices_of C & not v is cut-vertex )
reconsider v9 = v2 as Vertex of the removeVertex of G,cv by GLIB_000:42;
reconsider v = v9 as Vertex of G by GLIB_000:42;
take v = v; ::_thesis: ( v in the_Vertices_of C & not v is cut-vertex )
thus  v in the_Vertices_of C ; ::_thesis: not v is cut-vertex
set G3 = the removeVertex of G,v;
A99: the_Vertices_of the removeVertex of G,v = (the_Vertices_of G) \ {v} by GLIB_000:47;
 not cv in {v} by A68, TARSKI:def_1;
then reconsider cv9 = cv as Vertex of the removeVertex of G,v by A99, XBOOLE_0:def_5;
A100: v2 <> a by A33, A98, GLIB_000:71;
A101: the_Vertices_of C = the removeVertex of G,cv .reachableFrom v9 by Lm16;
now__::_thesis:_for_y_being_Vertex_of_the_removeVertex_of_G,v_ex_W_being_Walk_of_the_removeVertex_of_G,v_st_W_is_Walk_from_cv9,y
let y be Vertex of the removeVertex of G,v; ::_thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
now__::_thesis:_ex_W_being_Walk_of_the_removeVertex_of_G,v_st_W_is_Walk_from_cv9,y
percases ( y = cv or y <> cv ) ;
suppose y = cv ; ::_thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
then  the removeVertex of G,v .walkOf y is_Walk_from cv9,y by GLIB_001:13;
hence  ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y ; ::_thesis: verum
end;
supposeA102: y <> cv ; ::_thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
now__::_thesis:_ex_W_being_Walk_of_the_removeVertex_of_G,v_st_W_is_Walk_from_cv9,y
percases ( y in the_Vertices_of C or not y in the_Vertices_of C ) ;
supposeA103: y in the_Vertices_of C ; ::_thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
 not a in {v2} by A100, TARSKI:def_1;
then A104: a in the_Vertices_of the removeVertex of C9,v2 by A69, XBOOLE_0:def_5;
 not y in {v2} by A99, XBOOLE_0:def_5;
then  y in the_Vertices_of the removeVertex of C9,v2 by A69, A103, XBOOLE_0:def_5;
then consider W being Walk of the removeVertex of C9,v2 such that
A105: W is_Walk_from y,a by A71, A104, Def1;
A106: ( W . 1 = y & W . (len W) = a ) by A105, GLIB_001:17;
A107: now__::_thesis:_not_v_in_W_.vertices()
assume  v in W .vertices() ; ::_thesis: contradiction
then  not v in {v2} by A69, XBOOLE_0:def_5;
hence  contradiction by TARSKI:def_1; ::_thesis: verum
end;
 not e in v .edgesInOut() by A33, A68, A100, GLIB_000:65;
then  e in (the_Edges_of G) \ (v .edgesInOut()) by A34, XBOOLE_0:def_5;
then  e in (the_Edges_of G) \ (G .edgesInOut {v}) by GLIB_000:def_40;
then  e in G .edgesBetween ((the_Vertices_of G) \ {v}) by GLIB_000:35;
then  e in the_Edges_of the removeVertex of G,v by GLIB_000:47;
then  e Joins cv,a, the removeVertex of G,v by A33, GLIB_000:73;
then A108: e Joins a,cv, the removeVertex of G,v by GLIB_000:14;
reconsider W = W as Walk of C by GLIB_001:167;
reconsider W = W as Walk of the removeVertex of G,cv by GLIB_001:167;
reconsider W = W as Walk of G by GLIB_001:167;
 not v in W .vertices() by A107, GLIB_001:98;
then reconsider W = W as Walk of the removeVertex of G,v by GLIB_001:171;
 W is_Walk_from y,a by A106, GLIB_001:17;
then  W .addEdge e is_Walk_from y,cv by A108, GLIB_001:66;
then  (W .addEdge e) .reverse() is_Walk_from cv,y by GLIB_001:23;
hence  ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y ; ::_thesis: verum
end;
supposeA109: not y in the_Vertices_of C ; ::_thesis: ex P being Walk of the removeVertex of G,v st P is_Walk_from cv9,y
reconsider y9 = y as Vertex of G by GLIB_000:42;
consider W being Walk of G such that
A110: W is_Walk_from cv,y9 by Def1;
set P = the Path of W;
A111: the Path of W is_Walk_from cv,y9 by A110, GLIB_001:160;
then A112: the Path of W . (len the Path of W) = y9 by GLIB_001:17;
A113: the Path of W . 1 = cv by A111, GLIB_001:17;
now__::_thesis:_not_v_in_the_Path_of_W_.vertices()
assume  v in the Path of W .vertices() ; ::_thesis: contradiction
then consider n being odd Element of NAT  such that
A114: n <= len the Path of W and
A115: the Path of W . n = v by GLIB_001:87;
set P2 = the Path of W .cut (n,(len the Path of W));
A116: the Path of W .cut (n,(len the Path of W)) is_Walk_from v,y9 by A112, A114, A115, GLIB_001:37;
 1 <= n by ABIAN:12;
then A117: 1 < n by A68, A113, A115, XXREAL_0:1;
now__::_thesis:_not_cv_in_(_the_Path_of_W_.cut_(n,(len_the_Path_of_W)))_.vertices()
assume  cv in ( the Path of W .cut (n,(len the Path of W))) .vertices() ; ::_thesis: contradiction
then consider m being odd Element of NAT  such that
A118: m <= len ( the Path of W .cut (n,(len the Path of W))) and
A119: ( the Path of W .cut (n,(len the Path of W))) . m = cv by GLIB_001:87;
 1 <= m by ABIAN:12;
then A120: m in dom ( the Path of W .cut (n,(len the Path of W))) by A118, FINSEQ_3:25;
then A121: the Path of W . ((n + m) - 1) = cv by A114, A119, GLIB_001:47;
 1 + 1 < n + m by A117, ABIAN:12, XREAL_1:8;
then  (1 + 1) - 1 < (n + m) - 1 by XREAL_1:14;
then A122: (2 * 0) + 1 < (n + m) - 1 ;
A123: (n + m) - 1 in dom the Path of W by A114, A120, GLIB_001:47;
then  (n + m) - 1 <= len the Path of W by FINSEQ_3:25;
hence  contradiction by A102, A113, A112, A121, A123, A122, GLIB_001:def_28; ::_thesis: verum
end;
then reconsider P2 = the Path of W .cut (n,(len the Path of W)) as Walk of the removeVertex of G,cv by GLIB_001:171;
 P2 is_Walk_from v,y9 by A116, GLIB_001:19;
hence  contradiction by A101, A109, Def5; ::_thesis: verum
end;
then reconsider P = the Path of W as Walk of the removeVertex of G,v by GLIB_001:171;
take P = P; ::_thesis: P is_Walk_from cv9,y
thus  P is_Walk_from cv9,y by A111, GLIB_001:19; ::_thesis: verum
end;
end;
end;
hence  ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y ; ::_thesis: verum
end;
end;
end;
hence  ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y ; ::_thesis: verum
end;
then  the removeVertex of G,v is connected by Lm6;
then  the removeVertex of G,v .numComponents() = 1 by Lm18;
hence  not v is cut-vertex by A3, Def11; ::_thesis: verum
end;
suppose ( v1 in cv .allNeighbors() & v2 in cv .allNeighbors() ) ; ::_thesis: ex v being Vertex of G st
( v in the_Vertices_of C & not v is cut-vertex )
then consider e being set  such that
A124: e Joins cv,v2,G by GLIB_000:71;
reconsider v9 = v1 as Vertex of the removeVertex of G,cv by GLIB_000:42;
set a = v2;
reconsider v = v9 as Vertex of G by GLIB_000:42;
take v = v; ::_thesis: ( v in the_Vertices_of C & not v is cut-vertex )
thus  v in the_Vertices_of C ; ::_thesis: not v is cut-vertex
set G3 = the removeVertex of G,v;
A125: the_Vertices_of the removeVertex of G,v = (the_Vertices_of G) \ {v} by GLIB_000:47;
 not cv in {v} by A70, TARSKI:def_1;
then reconsider cv9 = cv as Vertex of the removeVertex of G,v by A125, XBOOLE_0:def_5;
A126: the_Vertices_of C = the removeVertex of G,cv .reachableFrom v9 by Lm16;
A127: e in the_Edges_of G by A124, GLIB_000:def_13;
now__::_thesis:_for_y_being_Vertex_of_the_removeVertex_of_G,v_ex_W_being_Walk_of_the_removeVertex_of_G,v_st_W_is_Walk_from_cv9,y
let y be Vertex of the removeVertex of G,v; ::_thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
now__::_thesis:_ex_W_being_Walk_of_the_removeVertex_of_G,v_st_W_is_Walk_from_cv9,y
percases ( y = cv or y <> cv ) ;
suppose y = cv ; ::_thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
then  the removeVertex of G,v .walkOf y is_Walk_from cv9,y by GLIB_001:13;
hence  ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y ; ::_thesis: verum
end;
supposeA128: y <> cv ; ::_thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
now__::_thesis:_ex_W_being_Walk_of_the_removeVertex_of_G,v_st_W_is_Walk_from_cv9,y
percases ( y in the_Vertices_of C or not y in the_Vertices_of C ) ;
supposeA129: y in the_Vertices_of C ; ::_thesis: ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y
 not v2 in {v1} by A63, TARSKI:def_1;
then A130: v2 in the_Vertices_of the removeVertex of C9,v1 by A67, XBOOLE_0:def_5;
 not y in {v1} by A125, XBOOLE_0:def_5;
then  y in the_Vertices_of the removeVertex of C9,v1 by A67, A129, XBOOLE_0:def_5;
then consider W being Walk of the removeVertex of C9,v1 such that
A131: W is_Walk_from y,v2 by A66, A130, Def1;
A132: ( W . 1 = y & W . (len W) = v2 ) by A131, GLIB_001:17;
A133: now__::_thesis:_not_v_in_W_.vertices()
assume  v in W .vertices() ; ::_thesis: contradiction
then  not v in {v1} by A67, XBOOLE_0:def_5;
hence  contradiction by TARSKI:def_1; ::_thesis: verum
end;
 not e in v .edgesInOut() by A63, A70, A124, GLIB_000:65;
then  e in (the_Edges_of G) \ (v .edgesInOut()) by A127, XBOOLE_0:def_5;
then  e in (the_Edges_of G) \ (G .edgesInOut {v}) by GLIB_000:def_40;
then  e in G .edgesBetween ((the_Vertices_of G) \ {v}) by GLIB_000:35;
then  e in the_Edges_of the removeVertex of G,v by GLIB_000:47;
then  e Joins cv,v2, the removeVertex of G,v by A124, GLIB_000:73;
then A134: e Joins v2,cv, the removeVertex of G,v by GLIB_000:14;
reconsider W = W as Walk of C by GLIB_001:167;
reconsider W = W as Walk of the removeVertex of G,cv by GLIB_001:167;
reconsider W = W as Walk of G by GLIB_001:167;
 not v in W .vertices() by A133, GLIB_001:98;
then reconsider W = W as Walk of the removeVertex of G,v by GLIB_001:171;
 W is_Walk_from y,v2 by A132, GLIB_001:17;
then  W .addEdge e is_Walk_from y,cv by A134, GLIB_001:66;
then  (W .addEdge e) .reverse() is_Walk_from cv,y by GLIB_001:23;
hence  ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y ; ::_thesis: verum
end;
supposeA135: not y in the_Vertices_of C ; ::_thesis: ex P being Walk of the removeVertex of G,v st P is_Walk_from cv9,y
reconsider y9 = y as Vertex of G by GLIB_000:42;
consider W being Walk of G such that
A136: W is_Walk_from cv,y9 by Def1;
set P = the Path of W;
A137: the Path of W is_Walk_from cv,y9 by A136, GLIB_001:160;
then A138: the Path of W . (len the Path of W) = y9 by GLIB_001:17;
A139: the Path of W . 1 = cv by A137, GLIB_001:17;
now__::_thesis:_not_v_in_the_Path_of_W_.vertices()
assume  v in the Path of W .vertices() ; ::_thesis: contradiction
then consider n being odd Element of NAT  such that
A140: n <= len the Path of W and
A141: the Path of W . n = v by GLIB_001:87;
set P2 = the Path of W .cut (n,(len the Path of W));
A142: the Path of W .cut (n,(len the Path of W)) is_Walk_from v,y9 by A138, A140, A141, GLIB_001:37;
 1 <= n by ABIAN:12;
then A143: 1 < n by A70, A139, A141, XXREAL_0:1;
now__::_thesis:_not_cv_in_(_the_Path_of_W_.cut_(n,(len_the_Path_of_W)))_.vertices()
assume  cv in ( the Path of W .cut (n,(len the Path of W))) .vertices() ; ::_thesis: contradiction
then consider m being odd Element of NAT  such that
A144: m <= len ( the Path of W .cut (n,(len the Path of W))) and
A145: ( the Path of W .cut (n,(len the Path of W))) . m = cv by GLIB_001:87;
 1 <= m by ABIAN:12;
then A146: m in dom ( the Path of W .cut (n,(len the Path of W))) by A144, FINSEQ_3:25;
then A147: the Path of W . ((n + m) - 1) = cv by A140, A145, GLIB_001:47;
 1 + 1 < n + m by A143, ABIAN:12, XREAL_1:8;
then  (1 + 1) - 1 < (n + m) - 1 by XREAL_1:14;
then A148: (2 * 0) + 1 < (n + m) - 1 ;
A149: (n + m) - 1 in dom the Path of W by A140, A146, GLIB_001:47;
then  (n + m) - 1 <= len the Path of W by FINSEQ_3:25;
hence  contradiction by A128, A139, A138, A147, A149, A148, GLIB_001:def_28; ::_thesis: verum
end;
then reconsider P2 = the Path of W .cut (n,(len the Path of W)) as Walk of the removeVertex of G,cv by GLIB_001:171;
 P2 is_Walk_from v,y9 by A142, GLIB_001:19;
hence  contradiction by A126, A135, Def5; ::_thesis: verum
end;
then reconsider P = the Path of W as Walk of the removeVertex of G,v by GLIB_001:171;
take P = P; ::_thesis: P is_Walk_from cv9,y
thus  P is_Walk_from cv9,y by A137, GLIB_001:19; ::_thesis: verum
end;
end;
end;
hence  ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y ; ::_thesis: verum
end;
end;
end;
hence  ex W being Walk of the removeVertex of G,v st W is_Walk_from cv9,y ; ::_thesis: verum
end;
then  the removeVertex of G,v is connected by Lm6;
then  the removeVertex of G,v .numComponents() = 1 by Lm18;
hence  not v is cut-vertex by A3, Def11; ::_thesis: verum
end;
end;
end;
hence  ex v being Vertex of G st
( v in the_Vertices_of C & not v is cut-vertex ) ; ::_thesis: verum
end;
end;
end;
hence  ex v being Vertex of G st
( v in the_Vertices_of C & not v is cut-vertex ) ; ::_thesis: verum
end;
then consider v1 being Vertex of G such that
A150: v1 in the_Vertices_of the inducedSubgraph of the removeVertex of G,cv,C1 and
A151: not v1 is cut-vertex ;
consider v2 being Vertex of G such that
A152: v2 in the_Vertices_of the inducedSubgraph of the removeVertex of G,cv,C2 and
A153: not v2 is cut-vertex by A12;
take v1 = v1; ::_thesis: ex v2 being Vertex of G st
( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex )
take v2 = v2; ::_thesis: ( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex )
now__::_thesis:_not_v1_=_v2
 C2 is non empty Subset of (the_Vertices_of the removeVertex of G,cv) by Lm13;
then A154: the_Vertices_of the inducedSubgraph of the removeVertex of G,cv,C2 = C2 by GLIB_000:def_37;
 C1 is non empty Subset of (the_Vertices_of the removeVertex of G,cv) by Lm13;
then A155: the_Vertices_of the inducedSubgraph of the removeVertex of G,cv,C1 = C1 by GLIB_000:def_37;
assume  v1 = v2 ; ::_thesis: contradiction
then  the inducedSubgraph of the removeVertex of G,cv,C1 == the inducedSubgraph of the removeVertex of G,cv,C2 by A150, A152, Lm17;
hence  contradiction by A8, A155, A154, GLIB_000:def_34; ::_thesis: verum
end;
hence  v1 <> v2 ; ::_thesis: ( not v1 is cut-vertex & not v2 is cut-vertex )
thus  ( not v1 is cut-vertex & not v2 is cut-vertex ) by A151, A153; ::_thesis: verum
end;
end;
end;
hence  ex v1, v2 being Vertex of G st
( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex ) ; ::_thesis: verum
end;
hence  S1[k] ; ::_thesis: verum
end;
then A156: for k being Nat st ( for n being Nat st n < k holds
S1[n] ) holds
S1[k] ;
A157: for k being Nat holds S1[k] from NAT_1:sch_4(A156);
 G .order() = G .order() ;
hence  ex v1, v2 being Vertex of G st
( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex ) by A157; ::_thesis: verum
end;

registration
let G be finite non trivial connected _Graph;
cluster non cut-vertex for Element of the_Vertices_of G;
existence
 not for b1 being Vertex of G holds b1 is cut-vertex
proof
 ex v1, v2 being Vertex of G st
( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex ) by Lm21;
hence  not for b1 being Vertex of G holds b1 is cut-vertex ; ::_thesis: verum
end;
end;

Lm22:  for G being acyclic _Graph
for W being Path of G
for e being set st not e in W .edges() & e in (W .last()) .edgesInOut() holds
W .addEdge e is Path-like
proof
let G be acyclic _Graph; ::_thesis: for W being Path of G
for e being set st not e in W .edges() & e in (W .last()) .edgesInOut() holds
W .addEdge e is Path-like
let W be Path of G; ::_thesis: for e being set st not e in W .edges() & e in (W .last()) .edgesInOut() holds
W .addEdge e is Path-like
let e be set ; ::_thesis: ( not e in W .edges() & e in (W .last()) .edgesInOut() implies W .addEdge e is Path-like )
assume that
A1: not e in W .edges() and
A2: e in (W .last()) .edgesInOut() ; ::_thesis: W .addEdge e is Path-like
set v = (W .last()) .adj e;
set W2 = W .addEdge e;
A3: e Joins W .last() ,(W .last()) .adj e,G by A2, GLIB_000:67;
then A4: len (W .addEdge e) = (len W) + 2 by GLIB_001:64;
A5: W .addEdge e is Trail-like by A1, A2, GLIB_001:142;
now__::_thesis:_W_.addEdge_e_is_Path-like
percases ( W is trivial or not W is trivial ) ;
supposeA6: W is trivial ; ::_thesis: W .addEdge e is Path-like
then  for n being odd Element of NAT st 1 < n & n <= len W holds
W . n <> (W .last()) .adj e by GLIB_001:126;
hence  W .addEdge e is Path-like by A1, A3, A6, GLIB_001:150; ::_thesis: verum
end;
supposeA7: not W is trivial ; ::_thesis: W .addEdge e is Path-like
A8: now__::_thesis:_for_n_being_odd_Element_of_NAT_st_1_<_n_&_n_<=_len_W_holds_
W_._n_<>_(W_.last())_.adj_e
let n be odd Element of NAT ; ::_thesis: ( 1 < n & n <= len W implies W . n <> (W .last()) .adj e )
assume that
A9: 1 < n and
A10: n <= len W ; ::_thesis: W . n <> (W .last()) .adj e
now__::_thesis:_not_W_._n_=_(W_.last())_.adj_e
set W3 = (W .addEdge e) .cut (n,(len (W .addEdge e)));
assume A11: W . n = (W .last()) .adj e ; ::_thesis: contradiction
A12: n <= len (W .addEdge e) by A4, A10, NAT_1:12;
then A13: ((W .addEdge e) .cut (n,(len (W .addEdge e)))) .first() = (W .addEdge e) . n by GLIB_001:37;
now__::_thesis:_not_(W_.addEdge_e)_.cut_(n,(len_(W_.addEdge_e)))_is_trivial
assume  (W .addEdge e) .cut (n,(len (W .addEdge e))) is trivial ; ::_thesis: contradiction
then  len ((W .addEdge e) .cut (n,(len (W .addEdge e)))) = 1 by GLIB_001:126;
then  1 + n = (len (W .addEdge e)) + 1 by A12, GLIB_001:36;
then  (2 + (len W)) - (len W) <= (len W) - (len W) by A4, A10, XREAL_1:13;
then  2 <= 0 ;
hence  contradiction ; ::_thesis: verum
end;
then consider W4 being Path of (W .addEdge e) .cut (n,(len (W .addEdge e))) such that
A14: not W4 is trivial by A5, GLIB_001:166;
 ((W .addEdge e) .cut (n,(len (W .addEdge e)))) .last() = (W .addEdge e) . (len (W .addEdge e)) by A12, GLIB_001:37;
then A15: ((W .addEdge e) .cut (n,(len (W .addEdge e)))) .last() = (W .addEdge e) .last() by GLIB_001:def_7
.= (W .last()) .adj e by A3, GLIB_001:63 ;
 n in dom W by A9, A10, FINSEQ_3:25;
then  ((W .addEdge e) .cut (n,(len (W .addEdge e)))) .first() = (W .last()) .adj e by A3, A11, A13, GLIB_001:65;
then  W4 is_Walk_from (W .last()) .adj e,(W .last()) .adj e by A15, GLIB_001:def_32;
then  W4 is closed by GLIB_001:119;
then  W4 is Cycle-like by A14, GLIB_001:def_31;
hence  contradiction by Def2; ::_thesis: verum
end;
hence  W . n <> (W .last()) .adj e ; ::_thesis: verum
end;
now__::_thesis:_not_W_is_closed
assume  W is closed ; ::_thesis: contradiction
then  W is Cycle-like by A7, GLIB_001:def_31;
hence  contradiction by Def2; ::_thesis: verum
end;
hence  W .addEdge e is Path-like by A1, A3, A8, GLIB_001:150; ::_thesis: verum
end;
end;
end;
hence  W .addEdge e is Path-like ; ::_thesis: verum
end;

Lm23:  for G being finite non trivial acyclic _Graph st the_Edges_of G <> {} holds
ex v1, v2 being Vertex of G st
( v1 <> v2 & v1 is endvertex & v2 is endvertex & v2 in G .reachableFrom v1 )
proof
let G be finite non trivial acyclic _Graph; ::_thesis: ( the_Edges_of G <> {} implies ex v1, v2 being Vertex of G st
( v1 <> v2 & v1 is endvertex & v2 is endvertex & v2 in G .reachableFrom v1 ) )
assume A1: the_Edges_of G <> {} ; ::_thesis: ex v1, v2 being Vertex of G st
( v1 <> v2 & v1 is endvertex & v2 is endvertex & v2 in G .reachableFrom v1 )
defpred S1[ Nat] means  ex W being Path of G st len W = $1;
set e = choose (the_Edges_of G);
A2: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_
k_<=_2_*_((G_.order())_+_1)
let k be Nat; ::_thesis: ( S1[k] implies k <= 2 * ((G .order()) + 1) )
assume  S1[k] ; ::_thesis: k <= 2 * ((G .order()) + 1)
then consider P being Path of G such that
A3: len P = k ;
 2 * (len (P .vertexSeq())) <= 2 * ((G .order()) + 1) by GLIB_001:154, XREAL_1:64;
then  k + 1 <= 2 * ((G .order()) + 1) by A3, GLIB_001:def_14;
then  (k + 1) - 1 <= (2 * ((G .order()) + 1)) - 0 by XREAL_1:13;
hence  k <= 2 * ((G .order()) + 1) ; ::_thesis: verum
end;
set src = (the_Source_of G) . (choose (the_Edges_of G));
set tar = (the_Target_of G) . (choose (the_Edges_of G));
 choose (the_Edges_of G) Joins (the_Source_of G) . (choose (the_Edges_of G)),(the_Target_of G) . (choose (the_Edges_of G)),G by A1, GLIB_000:def_13;
then A4: len (G .walkOf (((the_Source_of G) . (choose (the_Edges_of G))),(choose (the_Edges_of G)),((the_Target_of G) . (choose (the_Edges_of G))))) = 3 by GLIB_001:14;
then A5: ex k being Nat st S1[k] ;
consider k being Nat such that
A6: ( S1[k] & ( for n being Nat st S1[n] holds
n <= k ) ) from NAT_1:sch_6(A2, A5);
consider W being Path of G such that
A7: len W = k and
A8: for n being Nat st S1[n] holds
n <= k by A6;
A9: len (W .reverse()) = k by A7, GLIB_001:21;
A10: 3 <= len W by A4, A7, A8;
then A11: not W is trivial by GLIB_001:125;
A12: now__::_thesis:_not_W_.first()_=_W_.last()
assume  W .first() = W .last() ; ::_thesis: contradiction
then  W is closed by GLIB_001:def_24;
then  W is Cycle-like by A11, GLIB_001:def_31;
hence  contradiction by Def2; ::_thesis: verum
end;
then A13: W is open by GLIB_001:def_24;
A14: now__::_thesis:_for_W_being_Path_of_G_st_len_W_=_k_&_W_is_open_holds_
W_.last()_is_endvertex
let W be Path of G; ::_thesis: ( len W = k & W is open implies W .last() is endvertex )
assume that
A15: len W = k and
A16: W is open ; ::_thesis: W .last() is endvertex
 2 + 1 <= len W by A4, A8, A15;
then  2 < len W by NAT_1:13;
then reconsider lenW2 = (len W) - (2 * 1) as odd Element of NAT by INT_1:5;
A17: lenW2 + 2 = len W ;
A18: not W is trivial by A7, A10, A15, GLIB_001:125;
now__::_thesis:_W_.last()_is_endvertex
 W .last() in W .vertices() by GLIB_001:88;
then  not W .last() is isolated by A18, GLIB_001:135;
then  (W .last()) .degree() <> 0 by GLIB_000:def_50;
then  card ((W .last()) .edgesInOut()) <> 0 by GLIB_000:19;
then  0 < card ((W .last()) .edgesInOut()) by NAT_1:3;
then A19: 0 + 1 <= card ((W .last()) .edgesInOut()) by NAT_1:13;
assume  not W .last() is endvertex ; ::_thesis: contradiction
then  (W .last()) .degree() <> 1 by GLIB_000:def_52;
then  card ((W .last()) .edgesInOut()) <> 1 by GLIB_000:19;
then  1 < card ((W .last()) .edgesInOut()) by A19, XXREAL_0:1;
then consider e1, e2 being set  such that
A20: e1 in (W .last()) .edgesInOut() and
A21: ( e2 in (W .last()) .edgesInOut() & e1 <> e2 ) by NAT_1:59;
now__::_thesis:_ex_e2_being_set_st_
(_e2_in_(W_.last())_.edgesInOut()_&_e2_<>_W_._(lenW2_+_1)_)
percases ( e1 = W . (lenW2 + 1) or e1 <> W . (lenW2 + 1) ) ;
supposeA22: e1 = W . (lenW2 + 1) ; ::_thesis: ex e2 being set st
( e2 in (W .last()) .edgesInOut() & e2 <> W . (lenW2 + 1) )
take e2 = e2; ::_thesis: ( e2 in (W .last()) .edgesInOut() & e2 <> W . (lenW2 + 1) )
thus  ( e2 in (W .last()) .edgesInOut() & e2 <> W . (lenW2 + 1) ) by A21, A22; ::_thesis: verum
end;
supposeA23: e1 <> W . (lenW2 + 1) ; ::_thesis: ex e1 being set st
( e1 in (W .last()) .edgesInOut() & e1 <> W . (lenW2 + 1) )
take e1 = e1; ::_thesis: ( e1 in (W .last()) .edgesInOut() & e1 <> W . (lenW2 + 1) )
thus  ( e1 in (W .last()) .edgesInOut() & e1 <> W . (lenW2 + 1) ) by A20, A23; ::_thesis: verum
end;
end;
end;
then consider e being set  such that
A24: e in (W .last()) .edgesInOut() and
A25: e <> W . (lenW2 + 1) ;
consider v being Vertex of G such that
A26: e Joins W .last() ,v,G by A24, GLIB_000:64;
now__::_thesis:_contradiction
percases ( v in W .vertices() or not v in W .vertices() ) ;
suppose v in W .vertices() ; ::_thesis: contradiction
then consider n being odd Element of NAT  such that
A27: n <= len W and
A28: W . n = v by GLIB_001:87;
set m = W .rfind n;
set W2 = W .cut ((W .rfind n),(len W));
A29: W .rfind n <= len W by A27, GLIB_001:def_22;
then  (W .cut ((W .rfind n),(len W))) .last() = W . (len W) by GLIB_001:37;
then A30: e Joins (W .cut ((W .rfind n),(len W))) .last() ,v,G by A26, GLIB_001:def_7;
 W . (W .rfind n) = v by A27, A28, GLIB_001:def_22;
then A31: (W .cut ((W .rfind n),(len W))) .first() = v by A29, GLIB_001:37;
A32: e in ((W .cut ((W .rfind n),(len W))) .last()) .edgesInOut() by A30, GLIB_000:62;
now__::_thesis:_contradiction
percases ( not e in (W .cut ((W .rfind n),(len W))) .edges() or e in (W .cut ((W .rfind n),(len W))) .edges() ) ;
supposeA33: not e in (W .cut ((W .rfind n),(len W))) .edges() ; ::_thesis: contradiction
A34: not (W .cut ((W .rfind n),(len W))) .addEdge e is trivial by A30, GLIB_001:132;
 ( ((W .cut ((W .rfind n),(len W))) .addEdge e) .first() = v & ((W .cut ((W .rfind n),(len W))) .addEdge e) .last() = v ) by A31, A30, GLIB_001:63;
then A35: (W .cut ((W .rfind n),(len W))) .addEdge e is closed by GLIB_001:def_24;
 (W .cut ((W .rfind n),(len W))) .addEdge e is Path-like by A32, A33, Lm22;
then  (W .cut ((W .rfind n),(len W))) .addEdge e is Cycle-like by A35, A34, GLIB_001:def_31;
hence  contradiction by Def2; ::_thesis: verum
end;
supposeA36: e in (W .cut ((W .rfind n),(len W))) .edges() ; ::_thesis: contradiction
 (W .cut ((W .rfind n),(len W))) .edges() c= W .edges() by GLIB_001:106;
then consider a being even Element of NAT  such that
A37: 1 <= a and
A38: a <= len W and
A39: W . a = e by A36, GLIB_001:99;
reconsider a1 = a - 1 as odd Element of NAT by A37, INT_1:5;
A40: a1 < (len W) - 0 by A38, XREAL_1:15;
 a < lenW2 + 2 by A38, XXREAL_0:1;
then  a + 1 <= (lenW2 + 1) + 1 by NAT_1:13;
then  a <= lenW2 + 1 by XREAL_1:6;
then A41: a < lenW2 + 1 by A25, A39, XXREAL_0:1;
 a1 + 1 = a ;
then A42: e Joins W . a1,W . (a1 + 2),G by A39, A40, GLIB_001:def_3;
now__::_thesis:_contradiction
percases ( ( W .last() = W . a1 & v = W . (a1 + 2) ) or ( W .last() = W . (a1 + 2) & v = W . a1 ) ) by A26, A42, GLIB_000:15;
suppose ( W .last() = W . a1 & v = W . (a1 + 2) ) ; ::_thesis: contradiction
then  W . (len W) = W . a1 by GLIB_001:def_7;
hence  contradiction by A16, A40, GLIB_001:147; ::_thesis: verum
end;
supposeA43: ( W .last() = W . (a1 + 2) & v = W . a1 ) ; ::_thesis: contradiction
 a1 < (lenW2 + 1) - 1 by A41, XREAL_1:14;
then A44: a1 + 2 < len W by A17, XREAL_1:8;
 W . (len W) = W . (a1 + 2) by A43, GLIB_001:def_7;
hence  contradiction by A16, A44, GLIB_001:147; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
supposeA45: not v in W .vertices() ; ::_thesis: contradiction
A46: len (W .addEdge e) = k + 2 by A15, A26, GLIB_001:64;
 W .addEdge e is Path-like by A16, A26, A45, GLIB_001:151;
then  k + 2 <= k + 0 by A8, A46;
hence  contradiction by XREAL_1:6; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
hence  W .last() is endvertex ; ::_thesis: verum
end;
 W is_Walk_from W .first() ,W .last() by GLIB_001:def_23;
then A47: W .last() in G .reachableFrom (W .first()) by Def5;
 W .reverse() is open by A13, GLIB_001:120;
then  (W .reverse()) .last() is endvertex by A14, A9;
then A48: W .first() is endvertex by GLIB_001:22;
 W .last() is endvertex by A7, A13, A14;
hence  ex v1, v2 being Vertex of G st
( v1 <> v2 & v1 is endvertex & v2 is endvertex & v2 in G .reachableFrom v1 ) by A12, A48, A47; ::_thesis: verum
end;

Lm24:  for G being finite non trivial Tree-like _Graph ex v1, v2 being Vertex of G st
( v1 <> v2 & v1 is endvertex & v2 is endvertex )
proof
let G be finite non trivial Tree-like _Graph; ::_thesis: ex v1, v2 being Vertex of G st
( v1 <> v2 & v1 is endvertex & v2 is endvertex )
consider v1, v2 being Vertex of G such that
A1: v1 <> v2 by GLIB_000:21;
consider W being Walk of G such that
A2: W is_Walk_from v1,v2 by Def1;
A3: now__::_thesis:_not_len_W_=_1
assume  len W = 1 ; ::_thesis: contradiction
then A4: W .last() = W . 1 by GLIB_001:def_7
.= W .first() by GLIB_001:def_6 ;
 W .first() = v1 by A2, GLIB_001:def_23;
hence  contradiction by A1, A2, A4, GLIB_001:def_23; ::_thesis: verum
end;
 1 <= len W by ABIAN:12;
then  1 < len W by A3, XXREAL_0:1;
then  1 + 1 <= len W by NAT_1:13;
then  1 + 1 in dom W by FINSEQ_3:25;
then  W . (2 * 1) in the_Edges_of G by GLIB_001:8;
then  ex v1, v2 being Vertex of G st
( v1 <> v2 & v1 is endvertex & v2 is endvertex & v2 in G .reachableFrom v1 ) by Lm23;
hence  ex v1, v2 being Vertex of G st
( v1 <> v2 & v1 is endvertex & v2 is endvertex ) ; ::_thesis: verum
end;

registration
let G be finite non trivial Tree-like _Graph;
cluster endvertex for Element of the_Vertices_of G;
existence
 ex b1 being Vertex of G st b1 is endvertex
proof
consider v1, v2 being Vertex of G such that
 v1 <> v2 and
A1: v1 is endvertex and
 v2 is endvertex by Lm24;
take  v1 ; ::_thesis: v1 is endvertex
thus  v1 is endvertex by A1; ::_thesis: verum
end;
end;

registration
let G be finite non trivial Tree-like _Graph;
let v be endvertex Vertex of G;
cluster  ->  Tree-like for inducedSubgraph of G,(the_Vertices_of G) \ {v},G .edgesBetween ((the_Vertices_of G) \ {v});
coherence
 for b1 being removeVertex of G,v holds b1 is Tree-like
proof
let G2 be removeVertex of G,v; ::_thesis: G2 is Tree-like
 G2 is connected by Lm5;
hence  G2 is Tree-like ; ::_thesis: verum
end;
end;

definition
let GSq be GraphSeq;
attrGSq is connected  means :Def12: :: GLIB_002:def 12
 for n being Nat holds GSq . n is connected ;
attrGSq is acyclic  means :Def13: :: GLIB_002:def 13
 for n being Nat holds GSq . n is acyclic ;
attrGSq is Tree-like  means :Def14: :: GLIB_002:def 14
 for n being Nat holds GSq . n is Tree-like ;
end;

:: deftheorem Def12 defines connected GLIB_002:def_12_:_
 for GSq being GraphSeq holds
( GSq is connected iff for n being Nat holds GSq . n is connected );

:: deftheorem Def13 defines acyclic GLIB_002:def_13_:_
 for GSq being GraphSeq holds
( GSq is acyclic iff for n being Nat holds GSq . n is acyclic );

:: deftheorem Def14 defines Tree-like GLIB_002:def_14_:_
 for GSq being GraphSeq holds
( GSq is Tree-like iff for n being Nat holds GSq . n is Tree-like );

registration
cluster Relation-like NAT -defined Function-like V27( NAT ) Graph-yielding trivial  ->  connected for set ;
coherence
 for b1 being GraphSeq st b1 is trivial holds
b1 is connected
proof
let GSq be GraphSeq; ::_thesis: ( GSq is trivial implies GSq is connected )
assume A1: GSq is trivial ; ::_thesis: GSq is connected
let n be Nat; :: according to GLIB_002:def_12 ::_thesis: GSq . n is connected
reconsider G = GSq . n as trivial _Graph by A1;
 G is connected ;
hence  GSq . n is connected ; ::_thesis: verum
end;
cluster Relation-like NAT -defined Function-like V27( NAT ) Graph-yielding loopless trivial  ->  Tree-like for set ;
coherence
 for b1 being GraphSeq st b1 is trivial & b1 is loopless holds
b1 is Tree-like
proof
let GSq be GraphSeq; ::_thesis: ( GSq is trivial & GSq is loopless implies GSq is Tree-like )
assume A2: ( GSq is trivial & GSq is loopless ) ; ::_thesis: GSq is Tree-like
let n be Nat; :: according to GLIB_002:def_14 ::_thesis: GSq . n is Tree-like
reconsider G = GSq . n as loopless trivial _Graph by A2;
 G is Tree-like ;
hence  GSq . n is Tree-like ; ::_thesis: verum
end;
cluster Relation-like NAT -defined Function-like V27( NAT ) Graph-yielding acyclic  ->  simple for set ;
coherence
 for b1 being GraphSeq st b1 is acyclic holds
b1 is simple
proof
let GSq be GraphSeq; ::_thesis: ( GSq is acyclic implies GSq is simple )
assume A3: GSq is acyclic ; ::_thesis: GSq is simple
now__::_thesis:_for_n_being_Nat_holds_GSq_._n_is_simple
let n be Nat; ::_thesis: GSq . n is simple
reconsider G = GSq . n as acyclic _Graph by A3, Def13;
 G is simple ;
hence  GSq . n is simple ; ::_thesis: verum
end;
hence  GSq is simple by GLIB_000:def_63; ::_thesis: verum
end;
cluster Relation-like NAT -defined Function-like V27( NAT ) Graph-yielding Tree-like  ->  connected acyclic for set ;
coherence
 for b1 being GraphSeq st b1 is Tree-like holds
( b1 is acyclic & b1 is connected )
proof
let GSq be GraphSeq; ::_thesis: ( GSq is Tree-like implies ( GSq is acyclic & GSq is connected ) )
assume A4: GSq is Tree-like ; ::_thesis: ( GSq is acyclic & GSq is connected )
now__::_thesis:_for_n_being_Nat_holds_
(_GSq_._n_is_acyclic_&_GSq_._n_is_connected_)
let n be Nat; ::_thesis: ( GSq . n is acyclic & GSq . n is connected )
reconsider G = GSq . n as Tree-like _Graph by A4, Def14;
 G is acyclic ;
hence  ( GSq . n is acyclic & GSq . n is connected ) ; ::_thesis: verum
end;
hence  ( GSq is acyclic & GSq is connected ) by Def12, Def13; ::_thesis: verum
end;
cluster Relation-like NAT -defined Function-like V27( NAT ) Graph-yielding connected acyclic  ->  Tree-like for set ;
coherence
 for b1 being GraphSeq st b1 is acyclic & b1 is connected holds
b1 is Tree-like
proof
let GSq be GraphSeq; ::_thesis: ( GSq is acyclic & GSq is connected implies GSq is Tree-like )
assume A5: ( GSq is acyclic & GSq is connected ) ; ::_thesis: GSq is Tree-like
let n be Nat; :: according to GLIB_002:def_14 ::_thesis: GSq . n is Tree-like
reconsider G = GSq . n as connected acyclic _Graph by A5, Def12, Def13;
 G is Tree-like ;
hence  GSq . n is Tree-like ; ::_thesis: verum
end;
end;

registration
cluster Relation-like NAT -defined Function-like V27( NAT ) Graph-yielding halting finite Tree-like for set ;
existence
 ex b1 being GraphSeq st
( b1 is halting & b1 is finite & b1 is Tree-like )
proof
set G = the finite Tree-like _Graph;
set F = NAT --> the finite Tree-like _Graph;
A1: dom (NAT --> the finite Tree-like _Graph) = NAT by FUNCOP_1:13;
reconsider F = NAT --> the finite Tree-like _Graph as ManySortedSet of NAT ;
now__::_thesis:_for_x_being_Nat_holds_F_._x_is__Graph
let x be Nat; ::_thesis: F . x is _Graph
 x in NAT by ORDINAL1:def_12;
then  F . x in rng F by A1, FUNCT_1:3;
then  F . x in { the finite Tree-like _Graph} by FUNCOP_1:8;
hence  F . x is _Graph by TARSKI:def_1; ::_thesis: verum
end;
then reconsider F = F as GraphSeq by GLIB_000:def_53;
 F . (1 + 1) in rng F by A1, FUNCT_1:3;
then  F . (1 + 1) in { the finite Tree-like _Graph} by FUNCOP_1:8;
then A2: F . (1 + 1) = the finite Tree-like _Graph by TARSKI:def_1;
take  F ; ::_thesis: ( F is halting & F is finite & F is Tree-like )
 F . 1 in rng F by A1, FUNCT_1:3;
then  F . 1 in { the finite Tree-like _Graph} by FUNCOP_1:8;
then  F . 1 = the finite Tree-like _Graph by TARSKI:def_1;
hence  F is halting by A2, GLIB_000:def_54; ::_thesis: ( F is finite & F is Tree-like )
now__::_thesis:_for_x_being_Nat_holds_
(_F_._x_is_finite_&_F_._x_is_Tree-like_)
let x be Nat; ::_thesis: ( F . x is finite & F . x is Tree-like )
 x in NAT by ORDINAL1:def_12;
then  F . x in rng F by A1, FUNCT_1:3;
then  F . x in { the finite Tree-like _Graph} by FUNCOP_1:8;
hence  ( F . x is finite & F . x is Tree-like ) by TARSKI:def_1; ::_thesis: verum
end;
hence  ( F is finite & F is Tree-like ) by Def14, GLIB_000:def_57; ::_thesis: verum
end;
end;

registration
let GSq be connected GraphSeq;
let n be Nat;
clusterGSq . n ->  connected for _Graph;
coherence
 for b1 being _Graph st b1 = GSq . n holds
b1 is connected by Def12;
end;

registration
let GSq be acyclic GraphSeq;
let n be Nat;
clusterGSq . n ->  acyclic for _Graph;
coherence
 for b1 being _Graph st b1 = GSq . n holds
b1 is acyclic by Def13;
end;

registration
let GSq be Tree-like GraphSeq;
let n be Nat;
clusterGSq . n ->  Tree-like for _Graph;
coherence
 for b1 being _Graph st b1 = GSq . n holds
b1 is Tree-like ;
end;

begin


theorem :: GLIB_002:1
canceled;

theorem Th2: :: GLIB_002:2
for G being non trivial connected _Graph
for v being Vertex of G holds not v is isolated
proof
let G be non trivial connected _Graph; ::_thesis: for v being Vertex of G holds not v is isolated
let v be Vertex of G; ::_thesis: not v is isolated
consider v1, v2 being Vertex of G such that
A1: v1 <> v2 by GLIB_000:21;
now__::_thesis:_ex_u_being_Vertex_of_G_st_u_<>_v
percases ( v1 = v or v1 <> v ) ;
suppose v1 = v ; ::_thesis: ex u being Vertex of G st u <> v
hence  ex u being Vertex of G st u <> v by A1; ::_thesis: verum
end;
suppose v1 <> v ; ::_thesis: ex u being Vertex of G st u <> v
hence  ex u being Vertex of G st u <> v ; ::_thesis: verum
end;
end;
end;
then consider u being Vertex of G such that
A2: u <> v ;
consider W being Walk of G such that
A3: W is_Walk_from u,v by Def1;
A4: W .first() = u by A3, GLIB_001:def_23;
A5: W .last() = v by A3, GLIB_001:def_23;
then  v in W .vertices() by GLIB_001:88;
hence  not v is isolated by A2, A4, A5, GLIB_001:127, GLIB_001:135; ::_thesis: verum
end;

theorem Th3: :: GLIB_002:3
for G1 being non trivial _Graph
for v being Vertex of G1
for G2 being removeVertex of G1,v st G2 is connected & ex e being set st
( e in v .edgesInOut() & not e Joins v,v,G1 ) holds
G1 is connected
proof
let G1 be non trivial _Graph; ::_thesis: for v being Vertex of G1
for G2 being removeVertex of G1,v st G2 is connected & ex e being set st
( e in v .edgesInOut() & not e Joins v,v,G1 ) holds
G1 is connected
let v be Vertex of G1; ::_thesis: for G2 being removeVertex of G1,v st G2 is connected & ex e being set st
( e in v .edgesInOut() & not e Joins v,v,G1 ) holds
G1 is connected
let G2 be removeVertex of G1,v; ::_thesis: ( G2 is connected & ex e being set st
( e in v .edgesInOut() & not e Joins v,v,G1 ) implies G1 is connected )
assume that
A1: G2 is connected and
A2: ex e being set st
( e in v .edgesInOut() & not e Joins v,v,G1 ) ; ::_thesis: G1 is connected
A3: now__::_thesis:_for_x_being_Vertex_of_G1_st_x_<>_v_holds_
x_in_the_Vertices_of_G2
let x be Vertex of G1; ::_thesis: ( x <> v implies x in the_Vertices_of G2 )
assume  x <> v ; ::_thesis: x in the_Vertices_of G2
then  not x in {v} by TARSKI:def_1;
then  x in (the_Vertices_of G1) \ {v} by XBOOLE_0:def_5;
hence  x in the_Vertices_of G2 by GLIB_000:47; ::_thesis: verum
end;
consider e being set  such that
A4: e in v .edgesInOut() and
A5: not e Joins v,v,G1 by A2;
set v3 = v .adj e;
 v <> v .adj e by A4, A5, GLIB_000:67;
then reconsider v39 = v .adj e as Vertex of G2 by A3;
A6: e Joins v,v .adj e,G1 by A4, GLIB_000:67;
then A7: e Joins v .adj e,v,G1 by GLIB_000:14;
now__::_thesis:_for_v1,_v2_being_Vertex_of_G1_ex_W_being_Walk_of_G1_st_W_is_Walk_from_v1,v2
let v1, v2 be Vertex of G1; ::_thesis: ex W being Walk of G1 st W is_Walk_from v1,v2
now__::_thesis:_ex_W_being_Walk_of_G1_st_W_is_Walk_from_v1,v2
percases ( v1 <> v or v1 = v ) ;
suppose v1 <> v ; ::_thesis: ex W being Walk of G1 st W is_Walk_from v1,v2
then reconsider v19 = v1 as Vertex of G2 by A3;
now__::_thesis:_ex_W_being_Walk_of_G1_st_W_is_Walk_from_v1,v2
percases ( v2 <> v or v2 = v ) ;
suppose v2 <> v ; ::_thesis: ex W being Walk of G1 st W is_Walk_from v1,v2
then reconsider v29 = v2 as Vertex of G2 by A3;
consider W9 being Walk of G2 such that
A8: W9 is_Walk_from v19,v29 by A1, Def1;
reconsider W = W9 as Walk of G1 by GLIB_001:167;
 W is_Walk_from v1,v2 by A8, GLIB_001:19;
hence  ex W being Walk of G1 st W is_Walk_from v1,v2 ; ::_thesis: verum
end;
supposeA9: v2 = v ; ::_thesis: ex W being Walk of G1 st W is_Walk_from v1,v2
consider W9 being Walk of G2 such that
A10: W9 is_Walk_from v19,v39 by A1, Def1;
reconsider W = W9 as Walk of G1 by GLIB_001:167;
 W is_Walk_from v1,v .adj e by A10, GLIB_001:19;
then  ( W .first() = v1 & W .last() = v .adj e ) by GLIB_001:def_23;
then  W .addEdge e is_Walk_from v1,v2 by A7, A9, GLIB_001:63;
hence  ex W being Walk of G1 st W is_Walk_from v1,v2 ; ::_thesis: verum
end;
end;
end;
hence  ex W being Walk of G1 st W is_Walk_from v1,v2 ; ::_thesis: verum
end;
supposeA11: v1 = v ; ::_thesis: ex W being Walk of G1 st W is_Walk_from v1,v2
now__::_thesis:_ex_W_being_Walk_of_G1_st_W_is_Walk_from_v1,v2
percases ( v2 <> v or v2 = v ) ;
suppose v2 <> v ; ::_thesis: ex W being Walk of G1 st W is_Walk_from v1,v2
then reconsider v29 = v2 as Vertex of G2 by A3;
set W1 = G1 .walkOf (v1,e,(v .adj e));
consider W29 being Walk of G2 such that
A12: W29 is_Walk_from v39,v29 by A1, Def1;
reconsider W2 = W29 as Walk of G1 by GLIB_001:167;
A13: W2 is_Walk_from v .adj e,v2 by A12, GLIB_001:19;
take W = (G1 .walkOf (v1,e,(v .adj e))) .append W2; ::_thesis: W is_Walk_from v1,v2
 G1 .walkOf (v1,e,(v .adj e)) is_Walk_from v1,v .adj e by A6, A11, GLIB_001:15;
hence  W is_Walk_from v1,v2 by A13, GLIB_001:31; ::_thesis: verum
end;
supposeA14: v2 = v ; ::_thesis: ex W being Walk of G1 st W is_Walk_from v1,v2
take W = G1 .walkOf v; ::_thesis: W is_Walk_from v1,v2
thus  W is_Walk_from v1,v2 by A11, A14, GLIB_001:13; ::_thesis: verum
end;
end;
end;
hence  ex W being Walk of G1 st W is_Walk_from v1,v2 ; ::_thesis: verum
end;
end;
end;
hence  ex W being Walk of G1 st W is_Walk_from v1,v2 ; ::_thesis: verum
end;
hence  G1 is connected by Def1; ::_thesis: verum
end;

theorem :: GLIB_002:4
for G1 being non trivial connected _Graph
for v being Vertex of G1
for G2 being removeVertex of G1,v st v is endvertex holds
G2 is connected by Lm5;

theorem Th5: :: GLIB_002:5
for G1 being connected _Graph
for W being Walk of G1
for e being set
for G2 being removeEdge of G1,e st W is Cycle-like & e in W .edges() holds
G2 is connected
proof
let G1 be connected _Graph; ::_thesis: for W being Walk of G1
for e being set
for G2 being removeEdge of G1,e st W is Cycle-like & e in W .edges() holds
G2 is connected
let W be Walk of G1; ::_thesis: for e being set
for G2 being removeEdge of G1,e st W is Cycle-like & e in W .edges() holds
G2 is connected
let e be set ; ::_thesis: for G2 being removeEdge of G1,e st W is Cycle-like & e in W .edges() holds
G2 is connected
let G2 be removeEdge of G1,e; ::_thesis: ( W is Cycle-like & e in W .edges() implies G2 is connected )
assume that
A1: W is Cycle-like and
A2: e in W .edges() ; ::_thesis: G2 is connected
reconsider v1 = (the_Source_of G1) . e, v2 = (the_Target_of G1) . e as Vertex of G1 by A2, FUNCT_2:5;
 e Joins v1,v2,G1 by A2, GLIB_000:def_13;
then consider X being Walk of G1 such that
A3: X is_Walk_from v1,v2 and
A4: not e in X .edges() by A1, A2, GLIB_001:157;
reconsider X2 = X as Walk of G2 by A4, GLIB_001:172;
A5: X2 is_Walk_from v1,v2 by A3, GLIB_001:19;
then A6: X2 .reverse() is_Walk_from v2,v1 by GLIB_001:23;
now__::_thesis:_for_u,_v_being_Vertex_of_G2_ex_W_being_Walk_of_G2_st_W_is_Walk_from_u,v
let u, v be Vertex of G2; ::_thesis: ex W being Walk of G2 st W is_Walk_from u,v
 the_Vertices_of G2 c= the_Vertices_of G1 ;
then reconsider u9 = u, v9 = v as Vertex of G1 by TARSKI:def_3;
consider C being Walk of G1 such that
A7: C is_Walk_from u9,v9 by Def1;
set P = the Path of C;
A8: the Path of C is_Walk_from u9,v9 by A7, GLIB_001:160;
then A9: the Path of C . (len the Path of C) = v by GLIB_001:17;
A10: the Path of C . 1 = u by A8, GLIB_001:17;
now__::_thesis:_ex_W_being_Walk_of_G2_st_W_is_Walk_from_u,v
percases ( e in the Path of C .edges() or not e in the Path of C .edges() ) ;
suppose e in the Path of C .edges() ; ::_thesis: ex W being Walk of G2 st W is_Walk_from u,v
then consider a, b being Vertex of G1, m being odd Element of NAT  such that
A11: m + 2 <= len the Path of C and
A12: a = the Path of C . m and
A13: e = the Path of C . (m + 1) and
A14: b = the Path of C . (m + 2) and
A15: e Joins a,b,G1 by GLIB_001:103;
set P1 = the Path of C .cut (1,m);
set P2 = the Path of C .cut ((m + 2),(len the Path of C));
A16: (m + 2) - 2 < (len the Path of C) - 0 by A11, XREAL_1:15;
then A17: m + 1 <= len the Path of C by NAT_1:13;
now__::_thesis:_not_e_in_(_the_Path_of_C_.cut_(1,m))_.edges()
assume  e in ( the Path of C .cut (1,m)) .edges() ; ::_thesis: contradiction
then consider x being even Element of NAT  such that
A18: 1 <= x and
A19: x <= len ( the Path of C .cut (1,m)) and
A20: ( the Path of C .cut (1,m)) . x = e by GLIB_001:99;
 x <= m by A16, A19, GLIB_001:45;
then A21: x < m + 1 by NAT_1:13;
 x in dom ( the Path of C .cut (1,m)) by A18, A19, FINSEQ_3:25;
then  the Path of C . x = e by A16, A20, GLIB_001:46;
hence  contradiction by A13, A17, A18, A21, GLIB_001:138; ::_thesis: verum
end;
then reconsider P19 = the Path of C .cut (1,m) as Walk of G2 by GLIB_001:172;
now__::_thesis:_not_e_in_(_the_Path_of_C_.cut_((m_+_2),(len_the_Path_of_C)))_.edges()
assume  e in ( the Path of C .cut ((m + 2),(len the Path of C))) .edges() ; ::_thesis: contradiction
then consider x being even Element of NAT  such that
A22: 1 <= x and
A23: x <= len ( the Path of C .cut ((m + 2),(len the Path of C))) and
A24: ( the Path of C .cut ((m + 2),(len the Path of C))) . x = e by GLIB_001:99;
reconsider x1 = x - 1 as odd Element of NAT by A22, INT_1:5;
A25: x1 < (len ( the Path of C .cut ((m + 2),(len the Path of C)))) - 0 by A23, XREAL_1:15;
then  (m + 2) + x1 in dom the Path of C by A11, GLIB_001:36;
then A26: (m + 2) + x1 <= len the Path of C by FINSEQ_3:25;
 x1 + 1 = x ;
then A27: e = the Path of C . ((m + 2) + x1) by A11, A24, A25, GLIB_001:36;
 m + 1 < (m + 1) + 1 by NAT_1:13;
then A28: (m + 1) + 0 < (m + 2) + x1 by NAT_1:2, XREAL_1:8;
 1 <= m + 1 by NAT_1:12;
hence  contradiction by A13, A27, A26, A28, GLIB_001:138; ::_thesis: verum
end;
then reconsider P29 = the Path of C .cut ((m + 2),(len the Path of C)) as Walk of G2 by GLIB_001:172;
reconsider a = a, b = b as Vertex of G2 by GLIB_000:51;
 1 <= m by ABIAN:12;
then  the Path of C .cut (1,m) is_Walk_from u,a by A10, A12, A16, GLIB_001:37, JORDAN12:2;
then A29: P19 is_Walk_from u,a by GLIB_001:19;
 the Path of C .cut ((m + 2),(len the Path of C)) is_Walk_from b,v by A9, A11, A14, GLIB_001:37;
then A30: P29 is_Walk_from b,v by GLIB_001:19;
now__::_thesis:_ex_W_being_Walk_of_G2_st_W_is_Walk_from_u,v
percases ( ( a = v1 & b = v2 ) or ( b = v1 & a = v2 ) ) by A15, GLIB_000:def_13;
suppose ( a = v1 & b = v2 ) ; ::_thesis: ex W being Walk of G2 st W is_Walk_from u,v
then  P19 .append X2 is_Walk_from u,b by A5, A29, GLIB_001:31;
then  (P19 .append X2) .append P29 is_Walk_from u,v by A30, GLIB_001:31;
hence  ex W being Walk of G2 st W is_Walk_from u,v ; ::_thesis: verum
end;
suppose ( b = v1 & a = v2 ) ; ::_thesis: ex W being Walk of G2 st W is_Walk_from u,v
then  P19 .append (X2 .reverse()) is_Walk_from u,b by A6, A29, GLIB_001:31;
then  (P19 .append (X2 .reverse())) .append P29 is_Walk_from u,v by A30, GLIB_001:31;
hence  ex W being Walk of G2 st W is_Walk_from u,v ; ::_thesis: verum
end;
end;
end;
hence  ex W being Walk of G2 st W is_Walk_from u,v ; ::_thesis: verum
end;
suppose not e in the Path of C .edges() ; ::_thesis: ex P being Walk of G2 st P is_Walk_from u,v
then reconsider P = the Path of C as Walk of G2 by GLIB_001:172;
take P = P; ::_thesis: P is_Walk_from u,v
thus  P is_Walk_from u,v by A8, GLIB_001:19; ::_thesis: verum
end;
end;
end;
hence  ex W being Walk of G2 st W is_Walk_from u,v ; ::_thesis: verum
end;
hence  G2 is connected by Def1; ::_thesis: verum
end;

theorem :: GLIB_002:6
for G being _Graph st ex v1 being Vertex of G st
for v2 being Vertex of G ex W being Walk of G st W is_Walk_from v1,v2 holds
G is connected by Lm6;

theorem :: GLIB_002:7
for G being trivial _Graph holds G is connected ;

theorem Th8: :: GLIB_002:8
for G1, G2 being _Graph st G1 == G2 & G1 is connected holds
G2 is connected
proof
let G1, G2 be _Graph; ::_thesis: ( G1 == G2 & G1 is connected implies G2 is connected )
assume that
A1: G1 == G2 and
A2: G1 is connected ; ::_thesis: G2 is connected
now__::_thesis:_for_u,_v_being_Vertex_of_G2_ex_W_being_Walk_of_G2_st_W_is_Walk_from_u,v
let u, v be Vertex of G2; ::_thesis: ex W being Walk of G2 st W is_Walk_from u,v
reconsider u9 = u, v9 = v as Vertex of G1 by A1, GLIB_000:def_34;
consider W9 being Walk of G1 such that
A3: W9 is_Walk_from u9,v9 by A2, Def1;
reconsider W = W9 as Walk of G2 by A1, GLIB_001:179;
take W = W; ::_thesis: W is_Walk_from u,v
thus  W is_Walk_from u,v by A3, GLIB_001:19; ::_thesis: verum
end;
hence  G2 is connected by Def1; ::_thesis: verum
end;

theorem :: GLIB_002:9
for G being _Graph
for v being Vertex of G holds v in G .reachableFrom v by Lm1;

theorem :: GLIB_002:10
for G being _Graph
for x, e, y being set
for v1 being Vertex of G st x in G .reachableFrom v1 & e Joins x,y,G holds
y in G .reachableFrom v1 by Lm2;

theorem :: GLIB_002:11
for G being _Graph
for v being Vertex of G holds G .edgesBetween (G .reachableFrom v) = G .edgesInOut (G .reachableFrom v)
proof
let G be _Graph; ::_thesis: for v being Vertex of G holds G .edgesBetween (G .reachableFrom v) = G .edgesInOut (G .reachableFrom v)
let v be Vertex of G; ::_thesis: G .edgesBetween (G .reachableFrom v) = G .edgesInOut (G .reachableFrom v)
set R = G .reachableFrom v;
now__::_thesis:_for_x_being_set_st_x_in_G_.edgesInOut_(G_.reachableFrom_v)_holds_
x_in_G_.edgesBetween_(G_.reachableFrom_v)
let x be set ; ::_thesis: ( x in G .edgesInOut (G .reachableFrom v) implies x in G .edgesBetween (G .reachableFrom v) )
set Sx = (the_Source_of G) . x;
set Tx = (the_Target_of G) . x;
assume A1: x in G .edgesInOut (G .reachableFrom v) ; ::_thesis: x in G .edgesBetween (G .reachableFrom v)
then reconsider Sx = (the_Source_of G) . x, Tx = (the_Target_of G) . x as Vertex of G by FUNCT_2:5;
now__::_thesis:_x_in_G_.edgesBetween_(G_.reachableFrom_v)
percases ( Sx in G .reachableFrom v or Tx in G .reachableFrom v ) by A1, GLIB_000:28;
supposeA2: Sx in G .reachableFrom v ; ::_thesis: x in G .edgesBetween (G .reachableFrom v)
then consider W being Walk of G such that
A3: W is_Walk_from v,Sx by Def5;
now__::_thesis:_Tx_in_G_.reachableFrom_v
 W .last() = Sx by A3, GLIB_001:def_23;
then A4: x Joins W .last() ,Tx,G by A1, GLIB_000:def_13;
assume A5: not Tx in G .reachableFrom v ; ::_thesis: contradiction
 W .first() = v by A3, GLIB_001:def_23;
then  W .addEdge x is_Walk_from v,Tx by A4, GLIB_001:63;
hence  contradiction by A5, Def5; ::_thesis: verum
end;
then A6: x in G .edgesInto (G .reachableFrom v) by A1, GLIB_000:def_26;
 x in G .edgesOutOf (G .reachableFrom v) by A1, A2, GLIB_000:def_27;
then  x in (G .edgesInto (G .reachableFrom v)) /\ (G .edgesOutOf (G .reachableFrom v)) by A6, XBOOLE_0:def_4;
hence  x in G .edgesBetween (G .reachableFrom v) by GLIB_000:def_29; ::_thesis: verum
end;
supposeA7: Tx in G .reachableFrom v ; ::_thesis: x in G .edgesBetween (G .reachableFrom v)
then consider W being Walk of G such that
A8: W is_Walk_from v,Tx by Def5;
now__::_thesis:_Sx_in_G_.reachableFrom_v
 W .last() = Tx by A8, GLIB_001:def_23;
then A9: x Joins W .last() ,Sx,G by A1, GLIB_000:def_13;
assume A10: not Sx in G .reachableFrom v ; ::_thesis: contradiction
 W .first() = v by A8, GLIB_001:def_23;
then  W .addEdge x is_Walk_from v,Sx by A9, GLIB_001:63;
hence  contradiction by A10, Def5; ::_thesis: verum
end;
then A11: x in G .edgesOutOf (G .reachableFrom v) by A1, GLIB_000:def_27;
 x in G .edgesInto (G .reachableFrom v) by A1, A7, GLIB_000:def_26;
then  x in (G .edgesInto (G .reachableFrom v)) /\ (G .edgesOutOf (G .reachableFrom v)) by A11, XBOOLE_0:def_4;
hence  x in G .edgesBetween (G .reachableFrom v) by GLIB_000:def_29; ::_thesis: verum
end;
end;
end;
hence  x in G .edgesBetween (G .reachableFrom v) ; ::_thesis: verum
end;
then  ( G .edgesBetween (G .reachableFrom v) c= G .edgesInOut (G .reachableFrom v) & G .edgesInOut (G .reachableFrom v) c= G .edgesBetween (G .reachableFrom v) ) by GLIB_000:33, TARSKI:def_3;
hence  G .edgesBetween (G .reachableFrom v) = G .edgesInOut (G .reachableFrom v) by XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: GLIB_002:12
for G being _Graph
for v1, v2 being Vertex of G st v1 in G .reachableFrom v2 holds
G .reachableFrom v1 = G .reachableFrom v2 by Lm3;

theorem :: GLIB_002:13
for G being _Graph
for v being Vertex of G
for W being Walk of G st v in W .vertices() holds
W .vertices() c= G .reachableFrom v by Lm4;

theorem :: GLIB_002:14
for G1 being _Graph
for G2 being Subgraph of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
G2 .reachableFrom v2 c= G1 .reachableFrom v1
proof
let G1 be _Graph; ::_thesis: for G2 being Subgraph of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
G2 .reachableFrom v2 c= G1 .reachableFrom v1
let G2 be Subgraph of G1; ::_thesis: for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
G2 .reachableFrom v2 c= G1 .reachableFrom v1
let v1 be Vertex of G1; ::_thesis: for v2 being Vertex of G2 st v1 = v2 holds
G2 .reachableFrom v2 c= G1 .reachableFrom v1
let v2 be Vertex of G2; ::_thesis: ( v1 = v2 implies G2 .reachableFrom v2 c= G1 .reachableFrom v1 )
assume A1: v1 = v2 ; ::_thesis: G2 .reachableFrom v2 c= G1 .reachableFrom v1
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in G2 .reachableFrom v2 or v in G1 .reachableFrom v1 )
assume  v in G2 .reachableFrom v2 ; ::_thesis: v in G1 .reachableFrom v1
then consider W being Walk of G2 such that
A2: W is_Walk_from v2,v by Def5;
reconsider W2 = W as Walk of G1 by GLIB_001:167;
 W2 is_Walk_from v1,v by A1, A2, GLIB_001:19;
hence  v in G1 .reachableFrom v1 by Def5; ::_thesis: verum
end;

theorem :: GLIB_002:15
for G being _Graph st ex v being Vertex of G st G .reachableFrom v = the_Vertices_of G holds
G is connected by Lm7;

theorem :: GLIB_002:16
for G being _Graph st G is connected holds
for v being Vertex of G holds G .reachableFrom v = the_Vertices_of G by Lm8;

theorem :: GLIB_002:17
for G1, G2 being _Graph
for v1 being Vertex of G1
for v2 being Vertex of G2 st G1 == G2 & v1 = v2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2 by Lm9;

theorem :: GLIB_002:18
for G being _Graph
for v being Vertex of G holds v in G .reachableDFrom v
proof
let G be _Graph; ::_thesis: for v being Vertex of G holds v in G .reachableDFrom v
let v be Vertex of G; ::_thesis: v in G .reachableDFrom v
 G .walkOf v is_Walk_from v,v by GLIB_001:13;
hence  v in G .reachableDFrom v by Def6; ::_thesis: verum
end;

theorem :: GLIB_002:19
for G being _Graph
for x, e, y being set
for v1 being Vertex of G st x in G .reachableDFrom v1 & e DJoins x,y,G holds
y in G .reachableDFrom v1
proof
let G be _Graph; ::_thesis: for x, e, y being set
for v1 being Vertex of G st x in G .reachableDFrom v1 & e DJoins x,y,G holds
y in G .reachableDFrom v1
let x, e, y be set ; ::_thesis: for v1 being Vertex of G st x in G .reachableDFrom v1 & e DJoins x,y,G holds
y in G .reachableDFrom v1
let v1 be Vertex of G; ::_thesis: ( x in G .reachableDFrom v1 & e DJoins x,y,G implies y in G .reachableDFrom v1 )
set RFV = G .reachableDFrom v1;
assume that
A1: x in G .reachableDFrom v1 and
A2: e DJoins x,y,G ; ::_thesis: y in G .reachableDFrom v1
consider W being directed Walk of G such that
A3: W is_Walk_from v1,x by A1, Def6;
 ( W .addEdge e is directed & W .addEdge e is_Walk_from v1,y ) by A2, A3, GLIB_001:123;
hence  y in G .reachableDFrom v1 by Def6; ::_thesis: verum
end;

theorem :: GLIB_002:20
for G being _Graph
for v being Vertex of G holds G .reachableDFrom v c= G .reachableFrom v
proof
let G be _Graph; ::_thesis: for v being Vertex of G holds G .reachableDFrom v c= G .reachableFrom v
let v be Vertex of G; ::_thesis: G .reachableDFrom v c= G .reachableFrom v
set RFD = G .reachableDFrom v;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in G .reachableDFrom v or x in G .reachableFrom v )
assume A1: x in G .reachableDFrom v ; ::_thesis: x in G .reachableFrom v
then reconsider x9 = x as Vertex of G ;
 ex W being directed Walk of G st W is_Walk_from v,x9 by A1, Def6;
hence  x in G .reachableFrom v by Def5; ::_thesis: verum
end;

theorem :: GLIB_002:21
for G1 being _Graph
for G2 being Subgraph of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
G2 .reachableDFrom v2 c= G1 .reachableDFrom v1
proof
let G1 be _Graph; ::_thesis: for G2 being Subgraph of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
G2 .reachableDFrom v2 c= G1 .reachableDFrom v1
let G2 be Subgraph of G1; ::_thesis: for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
G2 .reachableDFrom v2 c= G1 .reachableDFrom v1
let v1 be Vertex of G1; ::_thesis: for v2 being Vertex of G2 st v1 = v2 holds
G2 .reachableDFrom v2 c= G1 .reachableDFrom v1
let v2 be Vertex of G2; ::_thesis: ( v1 = v2 implies G2 .reachableDFrom v2 c= G1 .reachableDFrom v1 )
assume A1: v1 = v2 ; ::_thesis: G2 .reachableDFrom v2 c= G1 .reachableDFrom v1
now__::_thesis:_for_v_being_set_st_v_in_G2_.reachableDFrom_v2_holds_
v_in_G1_.reachableDFrom_v1
let v be set ; ::_thesis: ( v in G2 .reachableDFrom v2 implies v in G1 .reachableDFrom v1 )
assume  v in G2 .reachableDFrom v2 ; ::_thesis: v in G1 .reachableDFrom v1
then consider W being DWalk of G2 such that
A2: W is_Walk_from v2,v by Def6;
reconsider W = W as DWalk of G1 by GLIB_001:175;
 W is_Walk_from v1,v by A1, A2, GLIB_001:19;
hence  v in G1 .reachableDFrom v1 by Def6; ::_thesis: verum
end;
hence  G2 .reachableDFrom v2 c= G1 .reachableDFrom v1 by TARSKI:def_3; ::_thesis: verum
end;

theorem :: GLIB_002:22
for G1, G2 being _Graph
for v1 being Vertex of G1
for v2 being Vertex of G2 st G1 == G2 & v1 = v2 holds
G1 .reachableDFrom v1 = G2 .reachableDFrom v2
proof
let G1, G2 be _Graph; ::_thesis: for v1 being Vertex of G1
for v2 being Vertex of G2 st G1 == G2 & v1 = v2 holds
G1 .reachableDFrom v1 = G2 .reachableDFrom v2
let v1 be Vertex of G1; ::_thesis: for v2 being Vertex of G2 st G1 == G2 & v1 = v2 holds
G1 .reachableDFrom v1 = G2 .reachableDFrom v2
let v2 be Vertex of G2; ::_thesis: ( G1 == G2 & v1 = v2 implies G1 .reachableDFrom v1 = G2 .reachableDFrom v2 )
assume that
A1: G1 == G2 and
A2: v1 = v2 ; ::_thesis: G1 .reachableDFrom v1 = G2 .reachableDFrom v2
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_G1_.reachableDFrom_v1_implies_x_in_G2_.reachableDFrom_v2_)_&_(_x_in_G2_.reachableDFrom_v2_implies_x_in_G1_.reachableDFrom_v1_)_)
let x be set ; ::_thesis: ( ( x in G1 .reachableDFrom v1 implies x in G2 .reachableDFrom v2 ) & ( x in G2 .reachableDFrom v2 implies x in G1 .reachableDFrom v1 ) )
hereby  ::_thesis: ( x in G2 .reachableDFrom v2 implies x in G1 .reachableDFrom v1 )
assume  x in G1 .reachableDFrom v1 ; ::_thesis: x in G2 .reachableDFrom v2
then consider W being DWalk of G1 such that
A3: W is_Walk_from v2,x by A2, Def6;
reconsider W2 = W as DWalk of G2 by A1, GLIB_001:179, GLIB_001:181;
 W2 is_Walk_from v2,x by A3, GLIB_001:19;
hence  x in G2 .reachableDFrom v2 by Def6; ::_thesis: verum
end;
assume  x in G2 .reachableDFrom v2 ; ::_thesis: x in G1 .reachableDFrom v1
then consider W being DWalk of G2 such that
A4: W is_Walk_from v1,x by A2, Def6;
reconsider W2 = W as DWalk of G1 by A1, GLIB_001:179, GLIB_001:181;
 W2 is_Walk_from v1,x by A4, GLIB_001:19;
hence  x in G1 .reachableDFrom v1 by Def6; ::_thesis: verum
end;
hence  G1 .reachableDFrom v1 = G2 .reachableDFrom v2 by TARSKI:1; ::_thesis: verum
end;

theorem :: GLIB_002:23
for G1 being _Graph
for G2 being connected Subgraph of G1 st G2 is spanning holds
G1 is connected by Lm10;

theorem :: GLIB_002:24
for G being _Graph holds union (G .componentSet()) = the_Vertices_of G
proof
let G be _Graph; ::_thesis: union (G .componentSet()) = the_Vertices_of G
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_union_(G_.componentSet())_implies_x_in_the_Vertices_of_G_)_&_(_x_in_the_Vertices_of_G_implies_x_in_union_(G_.componentSet())_)_)
let x be set ; ::_thesis: ( ( x in union (G .componentSet()) implies x in the_Vertices_of G ) & ( x in the_Vertices_of G implies x in union (G .componentSet()) ) )
thus  ( x in union (G .componentSet()) implies x in the_Vertices_of G ) ; ::_thesis: ( x in the_Vertices_of G implies x in union (G .componentSet()) )
assume  x in the_Vertices_of G ; ::_thesis: x in union (G .componentSet())
then reconsider x9 = x as Vertex of G ;
set Y = G .reachableFrom x9;
 ( x in G .reachableFrom x9 & G .reachableFrom x9 in G .componentSet() ) by Def8, Lm1;
hence  x in union (G .componentSet()) by TARSKI:def_4; ::_thesis: verum
end;
hence  union (G .componentSet()) = the_Vertices_of G by TARSKI:1; ::_thesis: verum
end;

theorem :: GLIB_002:25
for G being _Graph holds
( G is connected iff G .componentSet() = {(the_Vertices_of G)} ) by Lm11;

theorem :: GLIB_002:26
for G1, G2 being _Graph st G1 == G2 holds
G1 .componentSet() = G2 .componentSet() by Lm12;

theorem :: GLIB_002:27
for G being _Graph
for x being set st x in G .componentSet() holds
x is non empty Subset of (the_Vertices_of G) by Lm13;

theorem :: GLIB_002:28
for G being _Graph holds
( G is connected iff G .numComponents() = 1 ) by Lm18;

theorem :: GLIB_002:29
for G1, G2 being _Graph st G1 == G2 holds
G1 .numComponents() = G2 .numComponents() by Lm12;

theorem :: GLIB_002:30
for G being _Graph holds
( G is Component of G iff G is connected )
proof
let G be _Graph; ::_thesis: ( G is Component of G iff G is connected )
thus  ( G is Component of G implies G is connected ) ; ::_thesis: ( G is connected implies G is Component of G )
A1: G is Subgraph of G by GLIB_000:40;
A2: now__::_thesis:_for_G2_being_connected_Subgraph_of_G_holds_not_G_c<_G2
given G2 being connected Subgraph of G such that A3: G c< G2 ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( the_Vertices_of G c< the_Vertices_of G2 or the_Edges_of G c< the_Edges_of G2 ) by A1, A3, GLIB_000:98;
suppose the_Vertices_of G c< the_Vertices_of G2 ; ::_thesis: contradiction
hence  contradiction by XBOOLE_0:def_8; ::_thesis: verum
end;
suppose the_Edges_of G c< the_Edges_of G2 ; ::_thesis: contradiction
hence  contradiction by XBOOLE_0:def_8; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
assume  G is connected ; ::_thesis: G is Component of G
hence  G is Component of G by A2, Def7, GLIB_000:40; ::_thesis: verum
end;

theorem :: GLIB_002:31
for G being _Graph
for C being Component of G holds the_Edges_of C = G .edgesBetween (the_Vertices_of C) by Lm14;

theorem :: GLIB_002:32
for G being _Graph
for C1, C2 being Component of G holds
( the_Vertices_of C1 = the_Vertices_of C2 iff C1 == C2 ) by Lm15;

theorem :: GLIB_002:33
for G being _Graph
for C being Component of G
for v being Vertex of G holds
( v in the_Vertices_of C iff the_Vertices_of C = G .reachableFrom v ) by Lm16;

theorem :: GLIB_002:34
for G being _Graph
for C1, C2 being Component of G
for v being set st v in the_Vertices_of C1 & v in the_Vertices_of C2 holds
C1 == C2 by Lm17;

theorem :: GLIB_002:35
for G being connected _Graph
for v being Vertex of G holds
( not v is cut-vertex iff for G2 being removeVertex of G,v holds G2 .numComponents() c= G .numComponents() ) by Lm19;

theorem :: GLIB_002:36
for G being connected _Graph
for v being Vertex of G
for G2 being removeVertex of G,v st not v is cut-vertex holds
G2 is connected by Lm20;

theorem :: GLIB_002:37
for G being finite non trivial connected _Graph ex v1, v2 being Vertex of G st
( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex ) by Lm21;

theorem Th38: :: GLIB_002:38
for G being _Graph
for v being Vertex of G st v is cut-vertex holds
not G is trivial
proof
let G be _Graph; ::_thesis: for v being Vertex of G st v is cut-vertex holds
not G is trivial
let v be Vertex of G; ::_thesis: ( v is cut-vertex implies not G is trivial )
assume A1: v is cut-vertex ; ::_thesis: not G is trivial
now__::_thesis:_not_G_is_trivial
assume  G is trivial ; ::_thesis: contradiction
then reconsider G9 = G as trivial _Graph ;
set G2 = the removeVertex of G9,v;
 ( G9 .numComponents() = 1 & the removeVertex of G9,v .numComponents() = 1 ) by Lm18;
then  1 in 1 by A1, Def10;
hence  contradiction ; ::_thesis: verum
end;
hence  not G is trivial ; ::_thesis: verum
end;

theorem :: GLIB_002:39
for G1, G2 being _Graph
for v1 being Vertex of G1
for v2 being Vertex of G2 st G1 == G2 & v1 = v2 & v1 is cut-vertex holds
v2 is cut-vertex
proof
let G1, G2 be _Graph; ::_thesis: for v1 being Vertex of G1
for v2 being Vertex of G2 st G1 == G2 & v1 = v2 & v1 is cut-vertex holds
v2 is cut-vertex
let v1 be Vertex of G1; ::_thesis: for v2 being Vertex of G2 st G1 == G2 & v1 = v2 & v1 is cut-vertex holds
v2 is cut-vertex
let v2 be Vertex of G2; ::_thesis: ( G1 == G2 & v1 = v2 & v1 is cut-vertex implies v2 is cut-vertex )
assume that
A1: G1 == G2 and
A2: v1 = v2 and
A3: v1 is cut-vertex ; ::_thesis: v2 is cut-vertex
A4: not G1 is trivial by A3, Th38;
then A5: not G2 is trivial by A1, GLIB_000:89;
let G2A be removeVertex of G2,v2; :: according to GLIB_002:def_10 ::_thesis: G2 .numComponents() in G2A .numComponents()
set G1A = the removeVertex of G1,v1;
 G1 .numComponents() = G2 .numComponents() by A1, Lm12;
then A6: G2 .numComponents() in the removeVertex of G1,v1 .numComponents() by A3, Def10;
the_Vertices_of the removeVertex of G1,v1 = (the_Vertices_of G1) \ {v2} by A2, A4, GLIB_000:47
.= (the_Vertices_of G2) \ {v2} by A1, GLIB_000:def_34 ;
then A7: the_Vertices_of G2A = the_Vertices_of the removeVertex of G1,v1 by A5, GLIB_000:47;
 G2 is Subgraph of G1 by A1, GLIB_000:87;
then A8: G2A is Subgraph of G1 by GLIB_000:43;
the_Edges_of the removeVertex of G1,v1 = G1 .edgesBetween ((the_Vertices_of G1) \ {v1}) by A4, GLIB_000:47
.= G1 .edgesBetween ((the_Vertices_of G2) \ {v2}) by A1, A2, GLIB_000:def_34
.= G2 .edgesBetween ((the_Vertices_of G2) \ {v2}) by A1, GLIB_000:90 ;
then  the_Edges_of G2A = the_Edges_of the removeVertex of G1,v1 by A5, GLIB_000:47;
hence  G2 .numComponents() in G2A .numComponents() by A6, A7, A8, Lm12, GLIB_000:86; ::_thesis: verum
end;

theorem Th40: :: GLIB_002:40
for G being finite connected _Graph holds G .order() <= (G .size()) + 1
proof
let G be finite connected _Graph; ::_thesis: G .order() <= (G .size()) + 1
defpred S1[ finite _Graph] means ( $1 is connected implies $1 .order() <= ($1 .size()) + 1 );
A1: now__::_thesis:_for_k_being_non_empty_Nat_st_(_for_Gk_being_finite__Graph_st_Gk_.order()_=_k_holds_
S1[Gk]_)_holds_
for_Gk1_being_finite__Graph_st_Gk1_.order()_=_k_+_1_holds_
S1[Gk1]
let k be non empty Nat; ::_thesis: ( ( for Gk being finite _Graph st Gk .order() = k holds
S1[Gk] ) implies for Gk1 being finite _Graph st Gk1 .order() = k + 1 holds
S1[Gk1] )
assume A2: for Gk being finite _Graph st Gk .order() = k holds
S1[Gk] ; ::_thesis: for Gk1 being finite _Graph st Gk1 .order() = k + 1 holds
S1[Gk1]
let Gk1 be finite _Graph; ::_thesis: ( Gk1 .order() = k + 1 implies S1[Gk1] )
assume A3: Gk1 .order() = k + 1 ; ::_thesis: S1[Gk1]
now__::_thesis:_(_Gk1_is_connected_implies_Gk1_.order()_<=_(Gk1_.size())_+_1_)
A4: now__::_thesis:_not_Gk1_.order()_=_1
assume  Gk1 .order() = 1 ; ::_thesis: contradiction
then  k + 1 = 0 + 1 by A3;
hence  contradiction ; ::_thesis: verum
end;
assume  Gk1 is connected ; ::_thesis: Gk1 .order() <= (Gk1 .size()) + 1
then reconsider Gk19 = Gk1 as finite non trivial connected _Graph by A4, GLIB_000:26;
consider v1, v2 being Vertex of Gk19 such that
 v1 <> v2 and
A5: not v1 is cut-vertex and
 not v2 is cut-vertex by Lm21;
set Gkb = the removeVertex of Gk19,v1;
A6: ( ( the removeVertex of Gk19,v1 .order()) + 1 = k + 1 & ( the removeVertex of Gk19,v1 .size()) + (card (v1 .edgesInOut())) = Gk1 .size() ) by A3, GLIB_000:48;
 not v1 is isolated by Th2;
then  v1 .edgesInOut() <> {} by GLIB_000:def_49;
then  0 < card (v1 .edgesInOut()) by NAT_1:3;
then A7: 0 + 1 <= card (v1 .edgesInOut()) by NAT_1:13;
 the removeVertex of Gk19,v1 is connected by A5, Lm20;
then  k <= ((Gk1 .size()) - (card (v1 .edgesInOut()))) + 1 by A2, A6;
then  k + 1 <= (((Gk1 .size()) + 1) - (card (v1 .edgesInOut()))) + (card (v1 .edgesInOut())) by A7, XREAL_1:7;
hence  Gk1 .order() <= (Gk1 .size()) + 1 by A3; ::_thesis: verum
end;
hence  S1[Gk1] ; ::_thesis: verum
end;
A8: for G being finite _Graph st G .order() = 1 holds
S1[G] by NAT_1:12;
 for G being finite _Graph holds S1[G] from GLIB_000:sch_1(A8, A1);
hence  G .order() <= (G .size()) + 1 ; ::_thesis: verum
end;

theorem :: GLIB_002:41
for G being acyclic _Graph holds G is simple ;

theorem :: GLIB_002:42
for G being acyclic _Graph
for W being Path of G
for e being set st not e in W .edges() & e in (W .last()) .edgesInOut() holds
W .addEdge e is Path-like by Lm22;

theorem :: GLIB_002:43
for G being finite non trivial acyclic _Graph st the_Edges_of G <> {} holds
ex v1, v2 being Vertex of G st
( v1 <> v2 & v1 is endvertex & v2 is endvertex & v2 in G .reachableFrom v1 ) by Lm23;

theorem Th44: :: GLIB_002:44
for G1, G2 being _Graph st G1 == G2 & G1 is acyclic holds
G2 is acyclic
proof
let G1, G2 be _Graph; ::_thesis: ( G1 == G2 & G1 is acyclic implies G2 is acyclic )
assume that
A1: G1 == G2 and
A2: G1 is acyclic ; ::_thesis: G2 is acyclic
reconsider G19 = G1 as acyclic _Graph by A2;
 G2 is Subgraph of G19 by A1, GLIB_000:87;
hence  G2 is acyclic ; ::_thesis: verum
end;

theorem :: GLIB_002:45
for G being finite non trivial Tree-like _Graph ex v1, v2 being Vertex of G st
( v1 <> v2 & v1 is endvertex & v2 is endvertex ) by Lm24;

theorem Th46: :: GLIB_002:46
for G being finite _Graph holds
( G is Tree-like iff ( G is acyclic & G .order() = (G .size()) + 1 ) )
proof
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 set  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_set_holds_not_e_in_the_Edges_of_T
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: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;
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_empty_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 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: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 empty Nat st S2[k] holds
S2[k + 1] ;
 for k being non empty 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_empty_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 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__::_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 set  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, Th3; ::_thesis: verum
end;
then A20: for k being non empty 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 by Def1; ::_thesis: verum
end;
then A23: S1[1] ;
 for k being non empty 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
end;

theorem :: GLIB_002:47
for G being finite _Graph holds
( G is Tree-like iff ( G is connected & G .order() = (G .size()) + 1 ) )
proof
let G be finite _Graph; ::_thesis: ( G is Tree-like iff ( G is connected & G .order() = (G .size()) + 1 ) )
thus  ( G is Tree-like implies ( G is connected & G .order() = (G .size()) + 1 ) ) by Th46; ::_thesis: ( G is connected & G .order() = (G .size()) + 1 implies G is Tree-like )
assume that
A1: G is connected and
A2: G .order() = (G .size()) + 1 ; ::_thesis: G is Tree-like
now__::_thesis:_G_is_acyclic
assume  not G is acyclic ; ::_thesis: contradiction
then consider W being Walk of G such that
A3: W is Cycle-like by Def2;
set e = choose (W .edges());
set G2 = the removeEdge of G,(choose (W .edges()));
A4: W .edges() <> {} by A3, GLIB_001:136;
then  choose (W .edges()) in W .edges() ;
then A5: ( the removeEdge of G,(choose (W .edges())) .order() = G .order() & ( the removeEdge of G,(choose (W .edges())) .size()) + 1 = G .size() ) by GLIB_000:52;
 the removeEdge of G,(choose (W .edges())) is connected by A1, A3, A4, Th5;
then  (( the removeEdge of G,(choose (W .edges())) .size()) + 1) + 1 <= (( the removeEdge of G,(choose (W .edges())) .size()) + 1) + 0 by A2, A5, Th40;
hence  contradiction by XREAL_1:6; ::_thesis: verum
end;
hence  G is Tree-like by A1; ::_thesis: verum
end;

theorem Th48: :: GLIB_002:48
for G1, G2 being _Graph st G1 == G2 & G1 is Tree-like holds
G2 is Tree-like
proof
let G1, G2 be _Graph; ::_thesis: ( G1 == G2 & G1 is Tree-like implies G2 is Tree-like )
assume  ( G1 == G2 & G1 is Tree-like ) ; ::_thesis: G2 is Tree-like
then  ( G2 is connected & G2 is acyclic ) by Th8, Th44;
hence  G2 is Tree-like ; ::_thesis: verum
end;

theorem :: GLIB_002:49
for G being _Graph
for x being set st G is_DTree_rooted_at x holds
x is Vertex of G
proof
let G be _Graph; ::_thesis: for x being set st G is_DTree_rooted_at x holds
x is Vertex of G
let x be set ; ::_thesis: ( G is_DTree_rooted_at x implies x is Vertex of G )
set v = the Vertex of G;
assume  G is_DTree_rooted_at x ; ::_thesis: x is Vertex of G
then  ex W being DWalk of G st W is_Walk_from x, the Vertex of G by Def4;
hence  x is Vertex of G by GLIB_001:18; ::_thesis: verum
end;

theorem :: GLIB_002:50
for G1, G2 being _Graph
for x being set st G1 == G2 & G1 is_DTree_rooted_at x holds
G2 is_DTree_rooted_at x
proof
let G1, G2 be _Graph; ::_thesis: for x being set st G1 == G2 & G1 is_DTree_rooted_at x holds
G2 is_DTree_rooted_at x
let x be set ; ::_thesis: ( G1 == G2 & G1 is_DTree_rooted_at x implies G2 is_DTree_rooted_at x )
assume that
A1: G1 == G2 and
A2: G1 is_DTree_rooted_at x ; ::_thesis: G2 is_DTree_rooted_at x
A3: now__::_thesis:_for_y_being_Vertex_of_G2_ex_W9_being_DWalk_of_G2_st_W9_is_Walk_from_x,y
let y be Vertex of G2; ::_thesis: ex W9 being DWalk of G2 st W9 is_Walk_from x,y
reconsider y9 = y as Vertex of G1 by A1, GLIB_000:def_34;
consider W being DWalk of G1 such that
A4: W is_Walk_from x,y9 by A2, Def4;
reconsider W9 = W as DWalk of G2 by A1, GLIB_001:179, GLIB_001:181;
take W9 = W9; ::_thesis: W9 is_Walk_from x,y
thus  W9 is_Walk_from x,y by A4, GLIB_001:19; ::_thesis: verum
end;
 G1 is Tree-like by A2, Def4;
then  G2 is Tree-like by A1, Th48;
hence  G2 is_DTree_rooted_at x by A3, Def4; ::_thesis: verum
end;