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

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 ;
createGraph v in G2 .allConnectedSG() by Th127;
then createGraph v is Subgraph of G1 by A1, Th124;
then the_Vertices_of (createGraph v) c= the_Vertices_of G1 by GLIB_000:def 32;
hence x in the_Vertices_of G1 by ZFMISC_1:31; :: thesis: verum

end;

then A2: the_Vertices_of G2 c= the_Vertices_of G1 by TARSKI:def 3;
A3: the_Edges_of G2 c= the_Edges_of G1

proof

per cases ( G2 is edgeless or not G2 is edgeless ) ;

suppose G2 is edgeless ; :: thesis: the_Edges_of G2 c= the_Edges_of G1

then the_Edges_of G2 = {} ;
hence the_Edges_of G2 c= the_Edges_of G1 by XBOOLE_1:2; :: thesis: verum

end;

suppose not G2 is edgeless ; :: thesis: the_Edges_of G2 c= the_Edges_of G1

then reconsider G3 = G2 as non edgeless _Graph ;

now :: thesis: for x being object st x in the_Edges_of G3 holds
x in the_Edges_of G1

let x be object ; :: thesis: ( x in the_Edges_of G3 implies x in the_Edges_of G1 )
assume x in the_Edges_of G3 ; :: thesis: x in the_Edges_of G1
then reconsider e = x as Edge of G3 ;
createGraph e in G2 .allConnectedSG() by Th128;
then createGraph e is Subgraph of G1 by A1, Th124;
then the_Edges_of (createGraph e) c= the_Edges_of G1 by GLIB_000:def 32;
then {e} c= the_Edges_of G1 by Th13;
hence x in the_Edges_of G1 by ZFMISC_1:31; :: thesis: verum

end;

hence the_Edges_of G2 c= the_Edges_of G1 by TARSKI:def 3; :: thesis: verum

end;

end;

end;

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

let e0 be set ; :: thesis: ( e0 in the_Edges_of G2 implies ( (the_Source_of G2) . e0 = (the_Source_of G1) . e0 & (the_Target_of G2) . e0 = (the_Target_of G1) . e0 ) )
assume A4: e0 in the_Edges_of G2 ; :: thesis: ( (the_Source_of G2) . e0 = (the_Source_of G1) . e0 & (the_Target_of G2) . e0 = (the_Target_of G1) . e0 )
then reconsider G3 = G2 as non edgeless _Graph ;
reconsider e = e0 as Edge of G3 by A4;
createGraph e in G2 .allConnectedSG() by Th128;
then A5: createGraph e is Subgraph of G1 by A1, Th124;
the_Edges_of (createGraph e) = {e} by Th13;
then A6: e0 in the_Edges_of (createGraph e) by TARSKI:def 1;
then ( (the_Source_of (createGraph e)) . e0 = (the_Source_of G1) . e0 & (the_Target_of (createGraph e)) . e0 = (the_Target_of G1) . e0 ) by A5, GLIB_000:def 32;
hence ( (the_Source_of G2) . e0 = (the_Source_of G1) . e0 & (the_Target_of G2) . e0 = (the_Target_of G1) . e0 ) by A6, GLIB_000:def 32; :: thesis: verum

end;

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