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:
A3: the_Vertices_of G1 = S by GLIB_000:def 37;
then consider xs being Vertex of G such that
A4: xs in S and
A5: x,xs are_adjacent by A2, Th49;
consider e being object such that
A6: e Joins x,xs,G by A5;
reconsider Sx = S \/ {x} as Subset of (the_Vertices_of G) ;
let u, v be Vertex of G2; :: according to GLIB_002:def 1 :: thesis:
A7: the_Vertices_of G2 = Sx by GLIB_000:def 37;
then A8: ( u in S or u in {x} ) by XBOOLE_0:def 3;
x in {x} by TARSKI:def 1;
then A9: x in Sx by XBOOLE_0:def 3;
A10: xs in Sx by A4, XBOOLE_0:def 3;
e Joins xs,x,G by A6;
then A11: e Joins xs,x,G2 by A9, A10, Th19;
then A12: e Joins x,xs,G2 ;
A13: ( v in S or v in {x} ) by A7, XBOOLE_0:def 3;
A14: G1 is inducedSubgraph of G2,S by Th30, XBOOLE_1:7;

per cases by A8, A13, TARSKI:def 1;

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

the_Vertices_of G1 = S by GLIB_000:def 37;
then consider W being Walk of G1 such that
A16: W is_Walk_from u,v by A1, A15;
reconsider W = W as Walk of G2 by A14, GLIB_001:167;
take W ; :: thesis:
thus W is_Walk_from u,v by A16; :: thesis:

end;

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

then consider W being Walk of G1 such that
A18: W is_Walk_from u,xs by A1, A3, A4;
reconsider W = W as Walk of G2 by A14, GLIB_001:167;
take W .append (G2 .walkOf (xs,e,x)) ; :: thesis:
A19: G2 .walkOf (xs,e,x) is_Walk_from xs,x by A11, GLIB_001:15;
W is_Walk_from u,xs by A18;
hence W .append (G2 .walkOf (xs,e,x)) is_Walk_from u,v by A17, A19, GLIB_001:31; :: thesis:

end;

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

then consider W being Walk of G1 such that
A21: W is_Walk_from xs,v by A1, A3, A4;
reconsider W = W as Walk of G2 by A14, GLIB_001:167;
take (G2 .walkOf (x,e,xs)) .append W ; :: thesis:
A22: G2 .walkOf (x,e,xs) is_Walk_from x,xs by A12, GLIB_001:15;
W is_Walk_from xs,v by A21;
hence (G2 .walkOf (x,e,xs)) .append W is_Walk_from u,v by A20, A22, GLIB_001:31; :: thesis:

end;

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

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

end;

end;