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;

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

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;

end;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 )

A12:
the_Vertices_of G2 c= the_Vertices_of G3
by A6, GLIB_000:def 32;( 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;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

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper 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;

end;

( 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

end;

( x in the_Vertices_of G3 & not x in the_Vertices_of G2 ) ; :: thesis: contradiction

end;

suppose
ex e being object st

( e in the_Edges_of G3 & not e in the_Edges_of G2 ) ; :: thesis: contradiction

( 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;

end;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: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( the_Vertices_of G3 = the_Vertices_of G2 or the_Vertices_of G3 <> the_Vertices_of G2 )
;

end;

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;( v1 in G .reachableFrom v & v2 in G .reachableFrom v ) by A1;

hence contradiction by A2, A14, A16, GLIB_000:32; :: thesis: verum

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;hence contradiction by A8, XBOOLE_0:6; :: thesis: verum

now :: thesis: for x, y being Vertex of G2 ex W being Walk of G2 st W is_Walk_from x,y

then
G2 is connected
;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;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

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