let G be _Graph; :: thesis:
let G0 be Subgraph of G; :: thesis:
let S be non empty Subset of (the_Vertices_of G); :: thesis:
let x be Vertex of G; :: thesis:
let G1 be inducedSubgraph of G,S; :: thesis:
let G2 be inducedSubgraph of G,(S \/ {x}); :: thesis:
assume that
A1: G1 is connected and
A2: x in G .AdjacentSet (the_Vertices_of G1) ; :: thesis:
let u, v be Vertex of G2; :: according to GLIB_002:def 1 :: thesis:
reconsider Sx = S \/ {x} as Subset of (the_Vertices_of G) ;
the_Vertices_of G2 = Sx by GLIB_000:def 39;
then A3: ( ( u in S or u in {x} ) & ( v in S or v in {x} ) ) by XBOOLE_0:def 3;
A4: G1 is inducedSubgraph of G2,S by Th30, XBOOLE_1:7;
A5: the_Vertices_of G1 = S by GLIB_000:def 39;
then consider xs being Vertex of G such that
A6: xs in S and
A7: x,xs are_adjacent by A2, Th50;
consider e being set such that
A8: e Joins x,xs,G by A7, Def3;
A9: e Joins xs,x,G by A8, GLIB_000:17;
x in {x} by TARSKI:def 1;
then ( x in Sx & xs in Sx ) by A6, XBOOLE_0:def 3;
then A10: e Joins xs,x,G2 by A9, Th19;
then A11: e Joins x,xs,G2 by GLIB_000:17;

per cases by A3, TARSKI:def 1;

suppose A12: ( u in S & v in S ) ; :: thesis:

the_Vertices_of G1 = S by GLIB_000:def 39;
then consider W being Walk of G1 such that
A13: W is_Walk_from u,v by A1, A12, GLIB_002:def 1;
reconsider W = W as Walk of G2 by A4, GLIB_001:168;
take W ; :: thesis:
thus W is_Walk_from u,v by A13, GLIB_001:20; :: thesis:

end;

suppose A14: ( u in S & v = x ) ; :: thesis:

then consider W being Walk of G1 such that
A15: W is_Walk_from u,xs by A1, A5, A6, GLIB_002:def 1;
reconsider W = W as Walk of G2 by A4, GLIB_001:168;
take WW = W .append (G2 .walkOf xs,e,x); :: thesis:
A16: W is_Walk_from u,xs by A15, GLIB_001:20;
G2 .walkOf xs,e,x is_Walk_from xs,x by A10, GLIB_001:16;
hence WW is_Walk_from u,v by A14, A16, GLIB_001:32; :: thesis:

end;

suppose A17: ( u = x & v in S ) ; :: thesis:

then consider W being Walk of G1 such that
A18: W is_Walk_from xs,v by A1, A5, A6, GLIB_002:def 1;
reconsider W = W as Walk of G2 by A4, GLIB_001:168;
take WW = (G2 .walkOf x,e,xs) .append W; :: thesis:
A19: W is_Walk_from xs,v by A18, GLIB_001:20;
G2 .walkOf x,e,xs is_Walk_from x,xs by A11, GLIB_001:16;
hence WW is_Walk_from u,v by A17, A19, GLIB_001:32; :: thesis:

end;

suppose ( u = x & v = x ) ; :: thesis:

then G2 .walkOf u is_Walk_from u,v by GLIB_001:14;
hence ex b₁ being Walk of G2 st b₁ is_Walk_from u,v ; :: thesis:

end;