let T be 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
for w1, w2 being Vertex of F st w1 <> w2 & w1 in the_Vertices_of C & w2 in the_Vertices_of C & w1 in v .allNeighbors() holds
not w2 in v .allNeighbors()
let v be Vertex of T; :: thesis: for F being removeVertex of T,v
for C being Component of F
for w1, w2 being Vertex of F st w1 <> w2 & w1 in the_Vertices_of C & w2 in the_Vertices_of C & w1 in v .allNeighbors() holds
not w2 in v .allNeighbors()
let F be removeVertex of T,v; :: thesis: for C being Component of F
for w1, w2 being Vertex of F st w1 <> w2 & w1 in the_Vertices_of C & w2 in the_Vertices_of C & w1 in v .allNeighbors() holds
not w2 in v .allNeighbors()
let C be Component of F; :: thesis: for w1, w2 being Vertex of F st w1 <> w2 & w1 in the_Vertices_of C & w2 in the_Vertices_of C & w1 in v .allNeighbors() holds
not w2 in v .allNeighbors()
let w1, w2 be Vertex of F; :: thesis: ( w1 <> w2 & w1 in the_Vertices_of C & w2 in the_Vertices_of C & w1 in v .allNeighbors() implies not w2 in v .allNeighbors() )
assume that
A1: w1 <> w2 and
A2: ( w1 in the_Vertices_of C & w2 in the_Vertices_of C ) and
A3: ( w1 in v .allNeighbors() & w2 in v .allNeighbors() ) ; :: thesis: contradiction
the_Vertices_of C = F .reachableFrom w1 by A2, GLIB_002:33;
then consider W9 being Walk of F such that
A5: W9 is_Walk_from w1,w2 by A2, GLIB_002:def 5;
( the_Vertices_of F = (the_Vertices_of T) \ {v} & v in the_Vertices_of T ) by GLIB_000:47;
then A6: not v in W9 .vertices() by ZFMISC_1:56;
reconsider W = W9 as Walk of T by GLIB_001:167;
set P8 = the Path of W;
consider e1 being object such that
A7: e1 Joins v,w1,T by A3, GLIB_000:71;
consider e2 being object such that
A8: e2 Joins v,w2,T by A3, GLIB_000:71;
A9: e2 Joins w2,v,T by A8, GLIB_000:14;
set P9 = the Path of W .addEdge e2;
set P = ( the Path of W .addEdge e2) .addEdge e1;
W is_Walk_from w1,w2 by A5, GLIB_001:19;
then A10: the Path of W is_Walk_from w1,w2 by GLIB_001:160;
then A11: e2 Joins the Path of W .last() ,v,T by A9, GLIB_001:def 23;
not v in W .vertices() by A6, GLIB_001:98;
then A12: not v in the Path of W .vertices() by GLIB_001:163, TARSKI:def 3;
( the Path of W .first() = w1 & the Path of W .last() = w2 ) by A10, GLIB_001:def 23;
then the Path of W is open by A1, GLIB_001:def 24;
then A13: the Path of W .addEdge e2 is Path-like by A11, A12, GLIB_001:151;
A14: the Path of W .addEdge e2 is_Walk_from w1,v by A9, A10, GLIB_001:66;
then A15: ( the Path of W .addEdge e2) .last() = v by GLIB_001:def 23;
then A17: ( the Path of W .addEdge e2) .addEdge e1 is trivial by A7, GLIB_001:132;
A18: ( the Path of W .addEdge e2) .addEdge e1 is closed by A7, A14, GLIB_001:66, GLIB_001:119;
A19: not e1 in ( the Path of W .addEdge e2) .edges()

proof

assume e1 in ( the Path of W .addEdge e2) .edges() ; :: thesis: contradiction
then e1 in ( the Path of W .edges()) \/ {e2} by A11, GLIB_001:111;

per cases then ( e1 in the Path of W .edges() or e1 = e2 ) by ZFMISC_1:136;

suppose e1 in the Path of W .edges() ; :: thesis: contradiction

then e1 in W .edges() by GLIB_001:163, TARSKI:def 3;
then v in W .vertices() by A7, GLIB_001:105;
hence contradiction by A6, GLIB_001:98; :: thesis: verum

end;

suppose e1 = e2 ; :: thesis: contradiction

then W9 is_Walk_from v,w2 by A1, A5, A7, A8, GLIB_000:15;
then W9 .first() = v by GLIB_001:def 23;
hence contradiction by A6, GLIB_001:88; :: thesis: verum

end;

end;

end;

e1 in (( the Path of W .addEdge e2) .last()) .edgesInOut() by A7, A15, GLIB_000:62;
then ( the Path of W .addEdge e2) .addEdge e1 is Path-like by A13, A19, GLIB_002:42;
hence contradiction by A17, A18; :: thesis: verum