let T be _finite non _trivial Tree-like _Graph; :: thesis: for v being Vertex of T
for F being removeVertex of T,v
for C being Component of F ex w being Vertex of T st
( w is endvertex & w in the_Vertices_of C )
let v be Vertex of T; :: thesis: for F being removeVertex of T,v
for C being Component of F ex w being Vertex of T st
( w is endvertex & w in the_Vertices_of C )
let F be removeVertex of T,v; :: thesis: for C being Component of F ex w being Vertex of T st
( w is endvertex & w in the_Vertices_of C )
let C be Component of F; :: thesis: ex w being Vertex of T st
( w is endvertex & w in the_Vertices_of C )
A1: the_Vertices_of C c= the_Vertices_of F ;
A2: the_Vertices_of F c= the_Vertices_of T ;

per cases ( C is _trivial or not C is _trivial ) ;

suppose C is _trivial ; :: thesis: ex w being Vertex of T st
( w is endvertex & w in the_Vertices_of C )

then consider w8 being Vertex of C such that
A4: the_Vertices_of C = {w8} by GLIB_000:22;
reconsider w9 = w8 as Vertex of F by A1, TARSKI:def 3;
reconsider w = w9 as Vertex of T by A2, TARSKI:def 3;
take w ; :: thesis: ( w is endvertex & w in the_Vertices_of C )
set P = T .pathBetween (v,w);
the_Vertices_of F = (the_Vertices_of T) \ {v} by GLIB_000:47;
then A6: v <> w by ZFMISC_1:56;
A7: len (T .pathBetween (v,w)) = 3

proof

assume len (T .pathBetween (v,w)) <> 3 ; :: thesis: contradiction

per cases then ( len (T .pathBetween (v,w)) < 3 or 3 < len (T .pathBetween (v,w)) ) by XXREAL_0:1;

suppose len (T .pathBetween (v,w)) < 3 ; :: thesis: contradiction

then (T .pathBetween (v,w)) .first() = (T .pathBetween (v,w)) .last() by GLIB_001:125, GLIB_001:127;
then v = (T .pathBetween (v,w)) .last() by HELLY:28;
hence contradiction by A6, HELLY:28; :: thesis: verum

end;

suppose A8: 3 < len (T .pathBetween (v,w)) ; :: thesis: contradiction

then reconsider m = (len (T .pathBetween (v,w))) - 2 as Element of NAT by XXREAL_0:2, INT_1:5;
A9: m < (len (T .pathBetween (v,w))) - 0 by XREAL_1:15;
A10: ( m is odd & 1 is odd ) by POLYFORM:4, POLYFORM:5;
then (T .pathBetween (v,w)) . (m + 1) Joins (T .pathBetween (v,w)) . m,(T .pathBetween (v,w)) . (m + 2),T by A9, GLIB_001:def 3;
then (T .pathBetween (v,w)) . (m + 1) Joins (T .pathBetween (v,w)) .last() ,(T .pathBetween (v,w)) . m,T by GLIB_000:14;
then A11: (T .pathBetween (v,w)) . (m + 1) Joins w,(T .pathBetween (v,w)) . m,T by HELLY:28;

per cases ( (T .pathBetween (v,w)) . m <> v or (T .pathBetween (v,w)) . m = v ) ;

suppose (T .pathBetween (v,w)) . m <> v ; :: thesis: contradiction

then A13: (T .pathBetween (v,w)) . m in (the_Vertices_of T) \ {v} by A9, A10, ZFMISC_1:56, GLIB_001:7;
w in (the_Vertices_of T) \ {v} by A6, ZFMISC_1:56;
then (T .pathBetween (v,w)) . (m + 1) in T .edgesBetween ((the_Vertices_of T) \ {v}) by A11, A13, GLIB_000:32;
then (T .pathBetween (v,w)) . (m + 1) in the_Edges_of F by GLIB_000:47;
then A14: (T .pathBetween (v,w)) . (m + 1) Joins w,(T .pathBetween (v,w)) . m,F by A11, GLIB_000:73;
A15: {w9} = F .reachableFrom w9 by A4, GLIB_002:33;
then w in F .reachableFrom w9 by TARSKI:def 1;
then (T .pathBetween (v,w)) . m in F .reachableFrom w9 by A14, GLIB_002:10;
then (T .pathBetween (v,w)) . (m + 1) Joins w,w,T by A15, A11, TARSKI:def 1;
hence contradiction by GLIB_000:18; :: thesis: verum

end;

suppose (T .pathBetween (v,w)) . m = v ; :: thesis: contradiction

then A16: (T .pathBetween (v,w)) . m = (T .pathBetween (v,w)) .first() by HELLY:28
.= (T .pathBetween (v,w)) . 1 ;
( 3 - 2 < m & m <= len (T .pathBetween (v,w)) ) by A8, A9, XREAL_1:9;
then m = len (T .pathBetween (v,w)) by A10, A16, GLIB_001:def 28;
hence contradiction ; :: thesis: verum

end;

end;

end;

end;

end;

then (T .pathBetween (v,w)) . (1 + 1) Joins (T .pathBetween (v,w)) . 1,(T .pathBetween (v,w)) . (1 + 2),T by POLYFORM:4, GLIB_001:def 3;
then (T .pathBetween (v,w)) . 2 Joins (T .pathBetween (v,w)) .first() ,(T .pathBetween (v,w)) .last() ,T by A7;
then (T .pathBetween (v,w)) . 2 Joins v,(T .pathBetween (v,w)) .last() ,T by HELLY:28;
then A17: (T .pathBetween (v,w)) . 2 Joins v,w,T by HELLY:28;
A18: not (T .pathBetween (v,w)) . 2 Joins w,w,T by GLIB_000:18;

now :: thesis: for x being object holds
( ( x in w .edgesInOut() implies x = (T .pathBetween (v,w)) . 2 ) & ( x = (T .pathBetween (v,w)) . 2 implies x in w .edgesInOut() ) )

let x be object ; :: thesis: ( ( x in w .edgesInOut() implies x = (T .pathBetween (v,w)) . 2 ) & ( x = (T .pathBetween (v,w)) . 2 implies x in w .edgesInOut() ) )

hereby :: thesis: ( x = (T .pathBetween (v,w)) . 2 implies x in w .edgesInOut() )

assume x in w .edgesInOut() ; :: thesis: x = (T .pathBetween (v,w)) . 2
then consider u being Vertex of T such that
A19: x Joins w,u,T by GLIB_000:64;
u = v

proof

assume u <> v ; :: thesis: contradiction
then A20: u in (the_Vertices_of T) \ {v} by ZFMISC_1:56;
w in (the_Vertices_of T) \ {v} by A6, ZFMISC_1:56;
then x in T .edgesBetween ((the_Vertices_of T) \ {v}) by A19, A20, GLIB_000:32;
then x in the_Edges_of F by GLIB_000:47;
then A21: x Joins w,u,F by A19, GLIB_000:73;
A22: {w9} = F .reachableFrom w9 by A4, GLIB_002:33;
then w in F .reachableFrom w9 by TARSKI:def 1;
then u in F .reachableFrom w9 by A21, GLIB_002:10;
then x Joins w,w,T by A19, A22, TARSKI:def 1;
hence contradiction by GLIB_000:18; :: thesis: verum

end;

then x Joins v,w,T by A19, GLIB_000:14;
hence x = (T .pathBetween (v,w)) . 2 by A17, GLIB_000:def 20; :: thesis: verum

end;

assume x = (T .pathBetween (v,w)) . 2 ; :: thesis: x in w .edgesInOut()
hence x in w .edgesInOut() by A17, GLIB_000:14, GLIB_000:62; :: thesis: verum

end;

then w .edgesInOut() = {((T .pathBetween (v,w)) . 2)} by TARSKI:def 1;
hence ( w is endvertex & w in the_Vertices_of C ) by A18, GLIB_000:def 51; :: thesis: verum

end;

suppose A23: not C is _trivial ; :: thesis: ex w being Vertex of T st
( w is endvertex & w in the_Vertices_of C )

the_Edges_of C <> {}

proof

assume the_Edges_of C = {} ; :: thesis: contradiction
then C .size() = 0 ;
then C .order() = 0 + 1 by GLIB_002:46;
hence contradiction by A23, GLIB_000:def 19; :: thesis: verum

end;

then consider w1, w2 being Vertex of C such that
A25: ( w1 <> w2 & w1 is endvertex & w2 is endvertex ) and
w2 in C .reachableFrom w1 by A23, GLIB_002:43;
( w1 in the_Vertices_of F & w2 in the_Vertices_of F ) by A1, TARSKI:def 3;

per cases then ( not w1 in v .allNeighbors() or not w2 in v .allNeighbors() ) by A25, Lm1;

suppose A26: not w1 in v .allNeighbors() ; :: thesis: ex w being Vertex of T st
( w is endvertex & w in the_Vertices_of C )

w1 in the_Vertices_of C ;
then reconsider w = w1 as Vertex of T by A2, TARSKI:def 3;
reconsider w9 = w1 as Vertex of F by A1, TARSKI:def 3;
take w ; :: thesis: ( w is endvertex & w in the_Vertices_of C )
consider e being object such that
A27: ( w1 .edgesInOut() = {e} & not e Joins w1,w1,C ) by A25, GLIB_000:def 51;
A28: not e Joins w,w,T by GLIB_000:18;
C is Subgraph of T by GLIB_000:43;
then A29: w1 .edgesInOut() c= w .edgesInOut() by GLIB_000:78;

now :: thesis: for x being object holds
( ( x in w .edgesInOut() implies x = e ) & ( x = e implies x in w .edgesInOut() ) )

let x be object ; :: thesis: ( ( x in w .edgesInOut() implies x = e ) & ( x = e implies x in w .edgesInOut() ) )

hereby :: thesis: ( x = e implies x in w .edgesInOut() )

assume x in w .edgesInOut() ; :: thesis: x = e
then consider u being Vertex of T such that
A30: x Joins w,u,T by GLIB_000:64;
w in u .allNeighbors() by A30, GLIB_000:14, GLIB_000:71;
then A31: u in (the_Vertices_of T) \ {v} by A26, ZFMISC_1:56;
w1 in the_Vertices_of F by A1, TARSKI:def 3;
then w in (the_Vertices_of T) \ {v} by GLIB_000:47;
then x in T .edgesBetween ((the_Vertices_of T) \ {v}) by A30, A31, GLIB_000:32;
then x in the_Edges_of F by GLIB_000:47;
then x Joins w9,u,F by A30, GLIB_000:73;
then x in w9 .edgesInOut() by GLIB_000:62;
then x in w1 .edgesInOut() by GLIBPRE0:44;
hence x = e by A27, TARSKI:def 1; :: thesis: verum

end;

assume x = e ; :: thesis: x in w .edgesInOut()
then x in w1 .edgesInOut() by A27, TARSKI:def 1;
hence x in w .edgesInOut() by A29; :: thesis: verum

end;

then {e} = w .edgesInOut() by TARSKI:def 1;
hence ( w is endvertex & w in the_Vertices_of C ) by A28, GLIB_000:def 51; :: thesis: verum

end;

suppose A26: not w2 in v .allNeighbors() ; :: thesis: ex w being Vertex of T st
( w is endvertex & w in the_Vertices_of C )

w2 in the_Vertices_of C ;
then reconsider w = w2 as Vertex of T by A2, TARSKI:def 3;
reconsider w9 = w2 as Vertex of F by A1, TARSKI:def 3;
take w ; :: thesis: ( w is endvertex & w in the_Vertices_of C )
consider e being object such that
A27: ( w2 .edgesInOut() = {e} & not e Joins w2,w2,C ) by A25, GLIB_000:def 51;
A28: not e Joins w,w,T by GLIB_000:18;
C is Subgraph of T by GLIB_000:43;
then A29: w2 .edgesInOut() c= w .edgesInOut() by GLIB_000:78;

now :: thesis: for x being object holds
( ( x in w .edgesInOut() implies x = e ) & ( x = e implies x in w .edgesInOut() ) )

let x be object ; :: thesis: ( ( x in w .edgesInOut() implies x = e ) & ( x = e implies x in w .edgesInOut() ) )

hereby :: thesis: ( x = e implies x in w .edgesInOut() )

assume x in w .edgesInOut() ; :: thesis: x = e
then consider u being Vertex of T such that
A30: x Joins w,u,T by GLIB_000:64;
w in u .allNeighbors() by A30, GLIB_000:14, GLIB_000:71;
then A31: u in (the_Vertices_of T) \ {v} by A26, ZFMISC_1:56;
w2 in the_Vertices_of F by A1, TARSKI:def 3;
then w in (the_Vertices_of T) \ {v} by GLIB_000:47;
then x in T .edgesBetween ((the_Vertices_of T) \ {v}) by A30, A31, GLIB_000:32;
then x in the_Edges_of F by GLIB_000:47;
then x Joins w9,u,F by A30, GLIB_000:73;
then x in w9 .edgesInOut() by GLIB_000:62;
then x in w2 .edgesInOut() by GLIBPRE0:44;
hence x = e by A27, TARSKI:def 1; :: thesis: verum

end;

assume x = e ; :: thesis: x in w .edgesInOut()
then x in w2 .edgesInOut() by A27, TARSKI:def 1;
hence x in w .edgesInOut() by A29; :: thesis: verum

end;

then {e} = w .edgesInOut() by TARSKI:def 1;
hence ( w is endvertex & w in the_Vertices_of C ) by A28, GLIB_000:def 51; :: thesis: verum

end;

end;

end;

end;