let G be _Graph; :: thesis: for G0 being Subgraph of G

for S being non empty Subset of (the_Vertices_of G)

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 (the_Vertices_of G1) holds

G2 is connected

let G0 be Subgraph of G; :: thesis: for S being non empty Subset of (the_Vertices_of G)

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 (the_Vertices_of G1) holds

G2 is connected

let S be non empty Subset of (the_Vertices_of G); :: 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 (the_Vertices_of G1) 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 (the_Vertices_of G1) 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 (the_Vertices_of G1) holds

G2 is connected

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

assume that

A1: G1 is connected and

A2: x in G .AdjacentSet (the_Vertices_of G1) ; :: 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

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: ex b_{1} being Walk of G2 st b_{1} 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 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;

for S being non empty Subset of (the_Vertices_of G)

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 (the_Vertices_of G1) holds

G2 is connected

let G0 be Subgraph of G; :: thesis: for S being non empty Subset of (the_Vertices_of G)

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 (the_Vertices_of G1) holds

G2 is connected

let S be non empty Subset of (the_Vertices_of G); :: 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 (the_Vertices_of G1) 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 (the_Vertices_of G1) 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 (the_Vertices_of G1) holds

G2 is connected

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

assume that

A1: G1 is connected and

A2: x in G .AdjacentSet (the_Vertices_of G1) ; :: 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

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: ex b

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
( ( u in S & v in S ) or ( u in S & v = x ) or ( u = x & v in S ) or ( u = x & v = x ) )
by A8, A13, TARSKI:def 1;

end;

suppose A15:
( u in S & v in S )
; :: thesis: ex b_{1} being Walk of G2 st b_{1} 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 A1, A15;

reconsider W = W as Walk of G2 by A14, GLIB_001:167;

take W ; :: thesis: W is_Walk_from u,v

thus W is_Walk_from u,v by A16; :: thesis: verum

end;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: W is_Walk_from u,v

thus W is_Walk_from u,v by A16; :: thesis: verum

suppose A17:
( u in S & v = x )
; :: thesis: ex b_{1} being Walk of G2 st b_{1} 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 A14, GLIB_001:167;

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 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: verum

end;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: W .append (G2 .walkOf (xs,e,x)) is_Walk_from u,v

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: verum

suppose A20:
( u = x & v in S )
; :: thesis: ex b_{1} being Walk of G2 st b_{1} 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 A14, GLIB_001:167;

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 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: verum

end;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: (G2 .walkOf (x,e,xs)) .append W is_Walk_from u,v

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: verum

suppose
( u = x & v = x )
; :: thesis: ex b_{1} being Walk of G2 st b_{1} is_Walk_from u,v

then
G2 .walkOf u is_Walk_from u,v
by GLIB_001:13;

hence ex b_{1} being Walk of G2 st b_{1} is_Walk_from u,v
; :: thesis: verum

end;hence ex b