let G1, G2 be _Graph; :: thesis: ( G2 .allComponents() c= G1 .allComponents() implies G2 is Subgraph of G1 )
assume A1: G2 .allComponents() c= G1 .allComponents() ; :: thesis: G2 is Subgraph of G1

now :: thesis: ( the_Vertices_of G2 c= the_Vertices_of G1 & the_Edges_of G2 c= the_Edges_of G1 & ( for e being set st e in the_Edges_of G2 holds
( (the_Source_of G2) . e = (the_Source_of G1) . e & (the_Target_of G2) . e = (the_Target_of G1) . e ) ) )

now :: thesis: for x being object st x in the_Vertices_of G2 holds
x in the_Vertices_of G1

let x be object ; :: thesis: ( x in the_Vertices_of G2 implies x in the_Vertices_of G1 )
assume x in the_Vertices_of G2 ; :: thesis: x in the_Vertices_of G1
then reconsider v = x as Vertex of G2 ;
set C = the plain inducedSubgraph of G2,(G2 .reachableFrom v);
the plain inducedSubgraph of G2,(G2 .reachableFrom v) in G2 .allComponents() by Th189;
then the plain inducedSubgraph of G2,(G2 .reachableFrom v) is Component of G1 by A1, Th189;
then A2: the_Vertices_of the plain inducedSubgraph of G2,(G2 .reachableFrom v) c= the_Vertices_of G1 by GLIB_000:def 32;
the_Vertices_of the plain inducedSubgraph of G2,(G2 .reachableFrom v) = G2 .reachableFrom v by GLIB_000:def 37;
then v in the_Vertices_of the plain inducedSubgraph of G2,(G2 .reachableFrom v) by GLIB_002:9;
hence x in the_Vertices_of G1 by A2; :: thesis: verum

end;

hence the_Vertices_of G2 c= the_Vertices_of G1 by TARSKI:def 3; :: thesis: ( the_Edges_of G2 c= the_Edges_of G1 & ( for e being set st e in the_Edges_of G2 holds
( (the_Source_of G2) . e = (the_Source_of G1) . e & (the_Target_of G2) . e = (the_Target_of G1) . e ) ) )

now :: thesis: for e being object st e in the_Edges_of G2 holds
e in the_Edges_of G1

let e be object ; :: thesis: ( e in the_Edges_of G2 implies e in the_Edges_of G1 )
set v = (the_Source_of G2) . e;
set w = (the_Target_of G2) . e;
assume e in the_Edges_of G2 ; :: thesis: e in the_Edges_of G1
then A3: e Joins (the_Source_of G2) . e,(the_Target_of G2) . e,G2 by GLIB_000:def 13;
then reconsider v = (the_Source_of G2) . e as Vertex of G2 by GLIB_000:13;
set H = the plain inducedSubgraph of G2,(G2 .reachableFrom v);
the_Vertices_of the plain inducedSubgraph of G2,(G2 .reachableFrom v) = G2 .reachableFrom v by GLIB_000:def 37;
then reconsider v9 = v as Vertex of the plain inducedSubgraph of G2,(G2 .reachableFrom v) by GLIB_002:9;
e in v .edgesInOut() by A3, GLIB_000:62;
then e in v9 .edgesInOut() by GLIBPRE0:44;
then A4: e in the_Edges_of the plain inducedSubgraph of G2,(G2 .reachableFrom v) ;
the plain inducedSubgraph of G2,(G2 .reachableFrom v) in G2 .allComponents() by Th189;
then the plain inducedSubgraph of G2,(G2 .reachableFrom v) is Subgraph of G1 by A1, Th189;
then the_Edges_of the plain inducedSubgraph of G2,(G2 .reachableFrom v) c= the_Edges_of G1 by GLIB_000:def 32;
hence e in the_Edges_of G1 by A4; :: thesis: verum

end;

hence the_Edges_of G2 c= the_Edges_of G1 by TARSKI:def 3; :: thesis: for e being set st e in the_Edges_of G2 holds
( (the_Source_of G2) . e = (the_Source_of G1) . e & (the_Target_of G2) . e = (the_Target_of G1) . e )
let e be set ; :: thesis: ( e in the_Edges_of G2 implies ( (the_Source_of G2) . e = (the_Source_of G1) . e & (the_Target_of G2) . e = (the_Target_of G1) . e ) )
set v = (the_Source_of G2) . e;
set w = (the_Target_of G2) . e;
assume e in the_Edges_of G2 ; :: thesis: ( (the_Source_of G2) . e = (the_Source_of G1) . e & (the_Target_of G2) . e = (the_Target_of G1) . e )
then A5: e DJoins (the_Source_of G2) . e,(the_Target_of G2) . e,G2 by GLIB_000:def 14;
then e Joins (the_Source_of G2) . e,(the_Target_of G2) . e,G2 by GLIB_000:16;
then reconsider v = (the_Source_of G2) . e as Vertex of G2 by GLIB_000:13;
set H = the plain inducedSubgraph of G2,(G2 .reachableFrom v);
the_Vertices_of the plain inducedSubgraph of G2,(G2 .reachableFrom v) = G2 .reachableFrom v by GLIB_000:def 37;
then reconsider v9 = v as Vertex of the plain inducedSubgraph of G2,(G2 .reachableFrom v) by GLIB_002:9;
e in v .edgesOut() by A5, GLIB_000:59;
then e in v9 .edgesOut() by GLIBPRE0:44;
then A6: e DJoins v,(the_Target_of G2) . e, the plain inducedSubgraph of G2,(G2 .reachableFrom v) by A5, GLIB_000:73;
the plain inducedSubgraph of G2,(G2 .reachableFrom v) in G2 .allComponents() by Th189;
then the plain inducedSubgraph of G2,(G2 .reachableFrom v) is Subgraph of G1 by A1, Th189;
then e DJoins v,(the_Target_of G2) . e,G1 by A6, GLIB_000:72;
hence ( (the_Source_of G2) . e = (the_Source_of G1) . e & (the_Target_of G2) . e = (the_Target_of G1) . e ) by GLIB_000:def 14; :: thesis: verum

end;

hence G2 is Subgraph of G1 by GLIB_000:def 32; :: thesis: verum