let G2 be inducedSubgraph of G,(G .reachableFrom v); :: thesis: G2 is Component-like
A1: the_Vertices_of G2 = G .reachableFrom v by GLIB_000:def 39;
A2: the_Edges_of G2 = G .edgesBetween (G .reachableFrom v) by GLIB_000:def 39;

A3: now

A4: v in the_Vertices_of G2 by A1, Lm1;
given G3 being connected Subgraph of G such that A5: G2 c< G3 ; :: thesis: contradiction
G2 c= G3 by A5, GLIB_000:def 38;
then A6: G2 is Subgraph of G3 by GLIB_000:def 37;
then A7: the_Vertices_of G2 c= the_Vertices_of G3 by GLIB_000:def 34;

A8: now

given x being set such that A9: x in the_Vertices_of G3 and
A10: not x in the_Vertices_of G2 ; :: thesis: contradiction
consider W being Walk of G3 such that
A11: W is_Walk_from v,x by A4, A7, A9, Def1;
reconsider W = W as Walk of G by GLIB_001:168;
W is_Walk_from v,x by A11, GLIB_001:20;
hence contradiction by A1, A10, Def5; :: thesis: verum

end;

A12: the_Vertices_of G2 c= the_Vertices_of G3 by A6, GLIB_000:def 34;

now

per cases ( ex x being set st
( x in the_Vertices_of G3 & not x in the_Vertices_of G2 ) or ex e being set st
( e in the_Edges_of G3 & not e in the_Edges_of G2 ) ) by A5, GLIB_000:102;

suppose ex x being set st
( x in the_Vertices_of G3 & not x in the_Vertices_of G2 ) ; :: thesis: contradiction

hence contradiction by A8; :: thesis: verum

end;

suppose ex e being set st
( e in the_Edges_of G3 & not e in the_Edges_of G2 ) ; :: thesis: contradiction

then consider e being set such that
A13: e in the_Edges_of G3 and
A14: not e in the_Edges_of G2 ;
set v1 = (the_Source_of G3) . e;
set v2 = (the_Target_of G3) . e;
A15: e Joins (the_Source_of G3) . e,(the_Target_of G3) . e,G3 by A13, GLIB_000:def 15;
then A16: e Joins (the_Source_of G3) . e,(the_Target_of G3) . e,G by GLIB_000:75;

now

per cases ( the_Vertices_of G3 = the_Vertices_of G2 or the_Vertices_of G3 <> the_Vertices_of G2 ) ;

suppose the_Vertices_of G3 = the_Vertices_of G2 ; :: thesis: contradiction

then reconsider v1 = (the_Source_of G3) . e, v2 = (the_Target_of G3) . e as Vertex of G2 by A15, GLIB_000:16;
( v1 in G .reachableFrom v & v2 in G .reachableFrom v ) by A1;
hence contradiction by A2, A14, A16, GLIB_000:35; :: thesis: verum

end;

suppose the_Vertices_of G3 <> the_Vertices_of G2 ; :: thesis: contradiction

then the_Vertices_of G2 c< the_Vertices_of G3 by A12, XBOOLE_0:def 8;
hence contradiction by A8, XBOOLE_0:6; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

now

let x, y be Vertex of G2; :: thesis: ex W being Walk of G2 st W is_Walk_from x,y
consider W1R being Walk of G such that
A17: W1R is_Walk_from v,x by A1, Def5;
consider W2 being Walk of G such that
A18: W2 is_Walk_from v,y by A1, Def5;
set W1 = W1R .reverse() ;
set W = (W1R .reverse() ) .append W2;
A19: W1R .reverse() is_Walk_from x,v by A17, GLIB_001:24;
then A20: (W1R .reverse() ) .append W2 is_Walk_from x,y by A18, GLIB_001:32;
A21: (W1R .reverse() ) .last() = v by A19, GLIB_001:def 23;
then A22: v in (W1R .reverse() ) .vertices() by GLIB_001:89;
A23: ((W1R .reverse() ) .append W2) .edges() c= G .edgesBetween (((W1R .reverse() ) .append W2) .vertices() ) by GLIB_001:110;
W2 .first() = v by A18, GLIB_001:def 23;
then ((W1R .reverse() ) .append W2) .vertices() = ((W1R .reverse() ) .vertices() ) \/ (W2 .vertices() ) by A21, GLIB_001:94;
then A24: v in ((W1R .reverse() ) .append W2) .vertices() by A22, XBOOLE_0:def 3;
then G .edgesBetween (((W1R .reverse() ) .append W2) .vertices() ) c= G .edgesBetween (the_Vertices_of G2) by A1, Lm4, GLIB_000:39;
then ((W1R .reverse() ) .append W2) .edges() c= G .edgesBetween (the_Vertices_of G2) by A23, XBOOLE_1:1;
then reconsider W = (W1R .reverse() ) .append W2 as Walk of G2 by A1, A2, A24, Lm4, GLIB_001:171;
take W = W; :: thesis: W is_Walk_from x,y
thus W is_Walk_from x,y by A20, GLIB_001:20; :: thesis: verum

end;

then G2 is connected by Def1;
hence G2 is Component-like by A3, Def7; :: thesis: verum