let G2 be inducedSubgraph of G,(); :: 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 () 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 ;
given G3 being connected Subgraph of G such that A5: G2 c< G3 ; :: thesis: contradiction
G2 c= G3 by ;
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 ;
hence contradiction by A1, A10, Def5; :: thesis: verum
end;
A12: the_Vertices_of G2 c= the_Vertices_of G3 by ;
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 ;
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 = () . e;
set v2 = () . e;
A15: e Joins () . e,() . e,G3 by ;
then A16: e Joins () . e,() . e,G by GLIB_000:72;
per cases ;
suppose the_Vertices_of G3 = the_Vertices_of G2 ; :: thesis: contradiction
then reconsider v1 = () . e, v2 = () . e as Vertex of G2 by ;
( v1 in G .reachableFrom v & v2 in G .reachableFrom v ) by A1;
hence contradiction by A2, A14, A16, GLIB_000:32; :: 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,yend;
then G2 is connected ;
hence G2 is Component-like by A3; :: thesis: verum