let G be _Graph; :: thesis: for G0 being Subgraph of G
for S being non empty Subset of ()
for x being Vertex of G
for G1 being inducedSubgraph of G,S
for G2 being inducedSubgraph of G,(S \/ {x}) st G1 is connected & x in G .AdjacentSet () holds
G2 is connected

let G0 be Subgraph of G; :: thesis: for S being non empty Subset of ()
for x being Vertex of G
for G1 being inducedSubgraph of G,S
for G2 being inducedSubgraph of G,(S \/ {x}) st G1 is connected & x in G .AdjacentSet () holds
G2 is connected

let S be non empty Subset of (); :: thesis: for x being Vertex of G
for G1 being inducedSubgraph of G,S
for G2 being inducedSubgraph of G,(S \/ {x}) st G1 is connected & x in G .AdjacentSet () holds
G2 is connected

let x be Vertex of G; :: thesis: for G1 being inducedSubgraph of G,S
for G2 being inducedSubgraph of G,(S \/ {x}) st G1 is connected & x in G .AdjacentSet () holds
G2 is connected

let G1 be inducedSubgraph of G,S; :: thesis: for G2 being inducedSubgraph of G,(S \/ {x}) st G1 is connected & x in G .AdjacentSet () holds
G2 is connected

let G2 be inducedSubgraph of G,(S \/ {x}); :: thesis: ( G1 is connected & x in G .AdjacentSet () implies G2 is connected )
assume that
A1: G1 is connected and
A2: x in G .AdjacentSet () ; :: thesis: G2 is connected
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
consider e being object such that
A6: e Joins x,xs,G by A5;
reconsider Sx = S \/ {x} as Subset of () ;
let u, v be Vertex of G2; :: according to GLIB_002:def 1 :: thesis: ex b1 being Walk of G2 st b1 is_Walk_from u,v
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 ;
e Joins xs,x,G by A6;
then A11: e Joins xs,x,G2 by ;
then A12: e Joins x,xs,G2 ;
A13: ( v in S or v in {x} ) by ;
A14: G1 is inducedSubgraph of G2,S by ;
per cases ( ( u in S & v in S ) or ( u in S & v = x ) or ( u = x & v in S ) or ( u = x & v = x ) ) by ;
suppose A15: ( u in S & v in S ) ; :: thesis: ex b1 being Walk of G2 st b1 is_Walk_from u,v
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 ;
reconsider W = W as Walk of G2 by ;
take W ; :: thesis: W is_Walk_from u,v
thus W is_Walk_from u,v by A16; :: thesis: verum
end;
suppose A17: ( u in S & v = x ) ; :: thesis: ex b1 being Walk of G2 st b1 is_Walk_from u,v
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 ;
take W .append (G2 .walkOf (xs,e,x)) ; :: thesis: W .append (G2 .walkOf (xs,e,x)) is_Walk_from u,v
A19: G2 .walkOf (xs,e,x) is_Walk_from xs,x by ;
W is_Walk_from u,xs by A18;
hence W .append (G2 .walkOf (xs,e,x)) is_Walk_from u,v by ; :: thesis: verum
end;
suppose A20: ( u = x & v in S ) ; :: thesis: ex b1 being Walk of G2 st b1 is_Walk_from u,v
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 ;
take (G2 .walkOf (x,e,xs)) .append W ; :: thesis: (G2 .walkOf (x,e,xs)) .append W is_Walk_from u,v
A22: G2 .walkOf (x,e,xs) is_Walk_from x,xs by ;
W is_Walk_from xs,v by A21;
hence (G2 .walkOf (x,e,xs)) .append W is_Walk_from u,v by ; :: thesis: verum
end;
suppose ( u = x & v = x ) ; :: thesis: ex b1 being Walk of G2 st b1 is_Walk_from u,v
end;
end;