let G1 be _Graph; :: thesis: for G2 being loopless _Graph st G2 .allTrees() c= G1 .allTrees() holds
G2 is Subgraph of G1
let G2 be loopless _Graph; :: thesis: ( G2 .allTrees() c= G1 .allTrees() implies G2 is Subgraph of G1 )
assume A1: G2 .allTrees() c= G1 .allTrees() ; :: 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 ;
set H = createGraph v;
createGraph v in G2 .allTrees() by Th142;
then createGraph v is Subgraph of G1 by A1, Th138;
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;

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

let x be object ; :: thesis: ( x in the_Edges_of G2 implies x in the_Edges_of G1 )
assume A3: x in the_Edges_of G2 ; :: thesis: x in the_Edges_of G1
then reconsider G9 = G2 as non edgeless _Graph ;
reconsider e = x as Edge of G9 by A3;
set H = createGraph e;
not e in G9 .loops() ;
then createGraph e in G2 .allTrees() by Th143;
then createGraph e is Subgraph of G1 by A1, Th138;
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;

then A4: the_Edges_of G2 c= the_Edges_of G1 by TARSKI:def 3;

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

let x be set ; :: thesis: ( x in the_Edges_of G2 implies ( (the_Source_of G2) . x = (the_Source_of G1) . x & (the_Target_of G2) . x = (the_Target_of G1) . x ) )
assume A5: x in the_Edges_of G2 ; :: thesis: ( (the_Source_of G2) . x = (the_Source_of G1) . x & (the_Target_of G2) . x = (the_Target_of G1) . x )
then reconsider G9 = G2 as non edgeless _Graph ;
reconsider e = x as Edge of G9 by A5;
set H = createGraph e;
not e in G9 .loops() ;
then createGraph e in G2 .allTrees() by Th143;
then A6: ( createGraph e is Subgraph of G1 & createGraph e is Subgraph of G2 ) by A1, Th138;
the_Edges_of (createGraph e) = {e} by Th13;
then A7: x in the_Edges_of (createGraph e) by TARSKI:def 1;
thus (the_Source_of G2) . x = (the_Source_of (createGraph e)) . x by A7, GLIB_000:def 32
.= (the_Source_of G1) . x by A6, A7, GLIB_000:def 32 ; :: thesis: (the_Target_of G2) . x = (the_Target_of G1) . x
thus (the_Target_of G2) . x = (the_Target_of (createGraph e)) . x by A7, GLIB_000:def 32
.= (the_Target_of G1) . x by A6, A7, GLIB_000:def 32 ; :: thesis: verum

end;

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