let G be _Graph; :: thesis: for C being Component of G

for v being Vertex of G holds

( v in the_Vertices_of C iff the_Vertices_of C = G .reachableFrom v )

let C be Component of G; :: thesis: for v being Vertex of G holds

( v in the_Vertices_of C iff the_Vertices_of C = G .reachableFrom v )

let v be Vertex of G; :: thesis: ( v in the_Vertices_of C iff the_Vertices_of C = G .reachableFrom v )

hence v in the_Vertices_of C by Lm1; :: thesis: verum

for v being Vertex of G holds

( v in the_Vertices_of C iff the_Vertices_of C = G .reachableFrom v )

let C be Component of G; :: thesis: for v being Vertex of G holds

( v in the_Vertices_of C iff the_Vertices_of C = G .reachableFrom v )

let v be Vertex of G; :: thesis: ( v in the_Vertices_of C iff the_Vertices_of C = G .reachableFrom v )

hereby :: thesis: ( the_Vertices_of C = G .reachableFrom v implies v in the_Vertices_of C )

assume
the_Vertices_of C = G .reachableFrom v
; :: thesis: v in the_Vertices_of Cassume A1:
v in the_Vertices_of C
; :: thesis: the_Vertices_of C = G .reachableFrom v

end;now :: thesis: for x being object holds

( ( x in the_Vertices_of C implies x in G .reachableFrom v ) & ( x in G .reachableFrom v implies x in the_Vertices_of C ) )

hence
the_Vertices_of C = G .reachableFrom v
by TARSKI:2; :: thesis: verum( ( x in the_Vertices_of C implies x in G .reachableFrom v ) & ( x in G .reachableFrom v implies x in the_Vertices_of C ) )

let x be object ; :: thesis: ( ( x in the_Vertices_of C implies x in G .reachableFrom v ) & ( x in G .reachableFrom v implies x in the_Vertices_of C ) )

then reconsider x9 = x as Vertex of G ;

A4: G .reachableFrom x9 = G .reachableFrom v by A3, Lm3;

set CX = the inducedSubgraph of G,(G .reachableFrom x9);

not C c< the inducedSubgraph of G,(G .reachableFrom x9) by Def7;

then A5: ( C == the inducedSubgraph of G,(G .reachableFrom x9) or not C c= the inducedSubgraph of G,(G .reachableFrom x9) ) by GLIB_000:def 36;

A6: the_Edges_of the inducedSubgraph of G,(G .reachableFrom x9) = G .edgesBetween (G .reachableFrom x9) by GLIB_000:def 37;

A13: the_Vertices_of the inducedSubgraph of G,(G .reachableFrom x9) = G .reachableFrom x9 by GLIB_000:def 37;

then A15: C is Subgraph of the inducedSubgraph of G,(G .reachableFrom x9) by A12, GLIB_000:44;

x in the_Vertices_of the inducedSubgraph of G,(G .reachableFrom x9) by A13, Lm1;

hence x in the_Vertices_of C by A5, A15, GLIB_000:def 34, GLIB_000:def 35; :: thesis: verum

end;hereby :: thesis: ( x in G .reachableFrom v implies x in the_Vertices_of C )

assume A3:
x in G .reachableFrom v
; :: thesis: x in the_Vertices_of Cassume
x in the_Vertices_of C
; :: thesis: x in G .reachableFrom v

then reconsider x9 = x as Vertex of C ;

consider W being Walk of C such that

A2: W is_Walk_from v,x9 by A1, Def1;

reconsider W = W as Walk of G by GLIB_001:167;

W is_Walk_from v,x by A2, GLIB_001:19;

hence x in G .reachableFrom v by Def5; :: thesis: verum

end;then reconsider x9 = x as Vertex of C ;

consider W being Walk of C such that

A2: W is_Walk_from v,x9 by A1, Def1;

reconsider W = W as Walk of G by GLIB_001:167;

W is_Walk_from v,x by A2, GLIB_001:19;

hence x in G .reachableFrom v by Def5; :: thesis: verum

then reconsider x9 = x as Vertex of G ;

A4: G .reachableFrom x9 = G .reachableFrom v by A3, Lm3;

set CX = the inducedSubgraph of G,(G .reachableFrom x9);

not C c< the inducedSubgraph of G,(G .reachableFrom x9) by Def7;

then A5: ( C == the inducedSubgraph of G,(G .reachableFrom x9) or not C c= the inducedSubgraph of G,(G .reachableFrom x9) ) by GLIB_000:def 36;

A6: the_Edges_of the inducedSubgraph of G,(G .reachableFrom x9) = G .edgesBetween (G .reachableFrom x9) by GLIB_000:def 37;

now :: thesis: for e being object st e in the_Edges_of C holds

e in the_Edges_of the inducedSubgraph of G,(G .reachableFrom x9)

then A12:
the_Edges_of C c= the_Edges_of the inducedSubgraph of G,(G .reachableFrom x9)
;e in the_Edges_of the inducedSubgraph of G,(G .reachableFrom x9)

let e be object ; :: thesis: ( e in the_Edges_of C implies e in the_Edges_of the inducedSubgraph of G,(G .reachableFrom x9) )

set v1 = (the_Source_of C) . e;

set v2 = (the_Target_of C) . e;

assume A7: e in the_Edges_of C ; :: thesis: e in the_Edges_of the inducedSubgraph of G,(G .reachableFrom x9)

then reconsider v1 = (the_Source_of C) . e, v2 = (the_Target_of C) . e as Vertex of C by FUNCT_2:5;

e Joins v1,v2,C by A7, GLIB_000:def 13;

then A8: e Joins v1,v2,G by GLIB_000:72;

consider W1 being Walk of C such that

A9: W1 is_Walk_from v,v1 by A1, Def1;

reconsider W1 = W1 as Walk of G by GLIB_001:167;

consider W2 being Walk of C such that

A10: W2 is_Walk_from v,v2 by A1, Def1;

reconsider W2 = W2 as Walk of G by GLIB_001:167;

W2 is_Walk_from v,v2 by A10, GLIB_001:19;

then A11: v2 in G .reachableFrom x9 by A4, Def5;

W1 is_Walk_from v,v1 by A9, GLIB_001:19;

then v1 in G .reachableFrom x9 by A4, Def5;

hence e in the_Edges_of the inducedSubgraph of G,(G .reachableFrom x9) by A6, A8, A11, GLIB_000:32; :: thesis: verum

end;set v1 = (the_Source_of C) . e;

set v2 = (the_Target_of C) . e;

assume A7: e in the_Edges_of C ; :: thesis: e in the_Edges_of the inducedSubgraph of G,(G .reachableFrom x9)

then reconsider v1 = (the_Source_of C) . e, v2 = (the_Target_of C) . e as Vertex of C by FUNCT_2:5;

e Joins v1,v2,C by A7, GLIB_000:def 13;

then A8: e Joins v1,v2,G by GLIB_000:72;

consider W1 being Walk of C such that

A9: W1 is_Walk_from v,v1 by A1, Def1;

reconsider W1 = W1 as Walk of G by GLIB_001:167;

consider W2 being Walk of C such that

A10: W2 is_Walk_from v,v2 by A1, Def1;

reconsider W2 = W2 as Walk of G by GLIB_001:167;

W2 is_Walk_from v,v2 by A10, GLIB_001:19;

then A11: v2 in G .reachableFrom x9 by A4, Def5;

W1 is_Walk_from v,v1 by A9, GLIB_001:19;

then v1 in G .reachableFrom x9 by A4, Def5;

hence e in the_Edges_of the inducedSubgraph of G,(G .reachableFrom x9) by A6, A8, A11, GLIB_000:32; :: thesis: verum

A13: the_Vertices_of the inducedSubgraph of G,(G .reachableFrom x9) = G .reachableFrom x9 by GLIB_000:def 37;

now :: thesis: for z being object st z in the_Vertices_of C holds

z in the_Vertices_of the inducedSubgraph of G,(G .reachableFrom x9)

then
the_Vertices_of C c= the_Vertices_of the inducedSubgraph of G,(G .reachableFrom x9)
;z in the_Vertices_of the inducedSubgraph of G,(G .reachableFrom x9)

let z be object ; :: thesis: ( z in the_Vertices_of C implies z in the_Vertices_of the inducedSubgraph of G,(G .reachableFrom x9) )

assume z in the_Vertices_of C ; :: thesis: z in the_Vertices_of the inducedSubgraph of G,(G .reachableFrom x9)

then consider W being Walk of C such that

A14: W is_Walk_from v,z by A1, Def1;

reconsider W = W as Walk of G by GLIB_001:167;

W is_Walk_from v,z by A14, GLIB_001:19;

hence z in the_Vertices_of the inducedSubgraph of G,(G .reachableFrom x9) by A13, A4, Def5; :: thesis: verum

end;assume z in the_Vertices_of C ; :: thesis: z in the_Vertices_of the inducedSubgraph of G,(G .reachableFrom x9)

then consider W being Walk of C such that

A14: W is_Walk_from v,z by A1, Def1;

reconsider W = W as Walk of G by GLIB_001:167;

W is_Walk_from v,z by A14, GLIB_001:19;

hence z in the_Vertices_of the inducedSubgraph of G,(G .reachableFrom x9) by A13, A4, Def5; :: thesis: verum

then A15: C is Subgraph of the inducedSubgraph of G,(G .reachableFrom x9) by A12, GLIB_000:44;

x in the_Vertices_of the inducedSubgraph of G,(G .reachableFrom x9) by A13, Lm1;

hence x in the_Vertices_of C by A5, A15, GLIB_000:def 34, GLIB_000:def 35; :: thesis: verum

hence v in the_Vertices_of C by Lm1; :: thesis: verum