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

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
A2: W1R is_Walk_from v,x by A1, Def5;
consider W2 being Walk of G such that
A3: W2 is_Walk_from v,y by A1, Def5;
set W1 = W1R .reverse() ;
set W = (W1R .reverse() ) .append W2;
A4: W1R .reverse() is_Walk_from x,v by A2, GLIB_001:24;
then A5: (W1R .reverse() ) .append W2 is_Walk_from x,y by A3, GLIB_001:32;
A6: ( (W1R .reverse() ) .last() = v & W2 .first() = v ) by A3, A4, GLIB_001:def 23;
then A7: ((W1R .reverse() ) .append W2) .vertices() = ((W1R .reverse() ) .vertices() ) \/ (W2 .vertices() ) by GLIB_001:94;
v in (W1R .reverse() ) .vertices() by A6, GLIB_001:89;
then A8: v in ((W1R .reverse() ) .append W2) .vertices() by A7, XBOOLE_0:def 3;
then A9: G .edgesBetween (((W1R .reverse() ) .append W2) .vertices() ) c= G .edgesBetween (the_Vertices_of G2) by A1, Lm4, GLIB_000:39;
((W1R .reverse() ) .append W2) .edges() c= G .edgesBetween (((W1R .reverse() ) .append W2) .vertices() ) by GLIB_001:110;
then ((W1R .reverse() ) .append W2) .edges() c= G .edgesBetween (the_Vertices_of G2) by A9, XBOOLE_1:1;
then reconsider W = (W1R .reverse() ) .append W2 as Walk of G2 by A1, A8, Lm4, GLIB_001:171;
take W = W; :: thesis: W is_Walk_from x,y
thus W is_Walk_from x,y by A5, GLIB_001:20; :: thesis: verum

end;

then A10: G2 is connected by Def1;

now

given G3 being connected Subgraph of G such that A11: G2 c< G3 ; :: thesis: contradiction
G2 c= G3 by A11, GLIB_000:def 38;
then A12: G2 is Subgraph of G3 by GLIB_000:def 37;
A13: v in the_Vertices_of G2 by A1, Lm1;
A14: the_Vertices_of G2 c= the_Vertices_of G3 by A12, GLIB_000:def 34;

A15: now

given x being set such that A16: ( x in the_Vertices_of G3 & not x in the_Vertices_of G2 ) ; :: thesis: contradiction
consider W being Walk of G3 such that
A17: W is_Walk_from v,x by A13, A14, A16, Def1;
reconsider W = W as Walk of G by GLIB_001:168;
W is_Walk_from v,x by A17, GLIB_001:20;
hence contradiction by A1, A16, Def5; :: thesis: verum

end;

A18: the_Vertices_of G2 c= the_Vertices_of G3 by A12, 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 A11, 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 A15; :: 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
A19: ( e in the_Edges_of G3 & not e in the_Edges_of G2 ) ;
set v1 = (the_Source_of G3) . e;
set v2 = (the_Target_of G3) . e;
A20: e Joins (the_Source_of G3) . e,(the_Target_of G3) . e,G3 by A19, GLIB_000:def 15;
then A21: 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 A20, GLIB_000:16;
( v1 in G .reachableFrom v & v2 in G .reachableFrom v ) by A1;
hence contradiction by A1, A19, A21, 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 A18, XBOOLE_0:def 8;
hence contradiction by A15, XBOOLE_0:6; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence G2 is Component-like by A10, Def7; :: thesis: verum