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 37;
A2: the_Edges_of G2 = G .edgesBetween (G .reachableFrom v) by GLIB_000:def 37;

A3: now :: thesis: for G3 being connected Subgraph of G holds not G2 c< G3

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 36;
then A6: G2 is Subgraph of G3 by GLIB_000:def 35;
then A7: the_Vertices_of G2 c= the_Vertices_of G3 by GLIB_000:def 32;

A8: now :: thesis: for x being object holds
( not x in the_Vertices_of G3 or x in the_Vertices_of G2 )

given x being object 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:167;
W is_Walk_from v,x by A11, GLIB_001:19;
hence contradiction by A1, A10, Def5; :: thesis: verum

end;

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

now :: thesis: contradiction

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

suppose ex x being object 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 object 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 13;
then A16: e Joins (the_Source_of G3) . e,(the_Target_of G3) . e,G by GLIB_000:72;

now :: thesis: contradiction

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:13;
( v1 in G .reachableFrom v & v2 in G .reachableFrom v ) by A1;
hence contradiction by A2, A14, A16, GLIB_000:32; :: 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 :: thesis: for x, y being Vertex of G2 ex W being Walk of G2 st W is_Walk_from x,y

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:23;
then A20: (W1R .reverse()) .append W2 is_Walk_from x,y by A18, GLIB_001:31;
A21: (W1R .reverse()) .last() = v by A19, GLIB_001:def 23;
then A22: v in (W1R .reverse()) .vertices() by GLIB_001:88;
A23: ((W1R .reverse()) .append W2) .edges() c= G .edgesBetween (((W1R .reverse()) .append W2) .vertices()) by GLIB_001:109;
W2 .first() = v by A18, GLIB_001:def 23;
then ((W1R .reverse()) .append W2) .vertices() = ((W1R .reverse()) .vertices()) \/ (W2 .vertices()) by A21, GLIB_001:93;
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:36;
then ((W1R .reverse()) .append W2) .edges() c= G .edgesBetween (the_Vertices_of G2) by A23;
then reconsider W = (W1R .reverse()) .append W2 as Walk of G2 by A1, A2, A24, Lm4, GLIB_001:170;
take W = W; :: thesis: W is_Walk_from x,y
thus W is_Walk_from x,y by A20, GLIB_001:19; :: thesis: verum

end;

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