let G1 be _Graph; :: thesis: for G2 being loopless _Graph st G2 .allSpanningForests() c= G1 .allSpanningForests() holds
G2 is spanning Subgraph of G1
let G2 be loopless _Graph; :: thesis: ( G2 .allSpanningForests() c= G1 .allSpanningForests() implies G2 is spanning Subgraph of G1 )
assume A1: G2 .allSpanningForests() c= G1 .allSpanningForests() ; :: thesis: G2 is spanning Subgraph of G1
set H0 = the spanning acyclic plain Subgraph of G2;
the spanning acyclic plain Subgraph of G2 in G2 .allSpanningForests() by Th102;
then the spanning acyclic plain Subgraph of G2 is spanning Subgraph of G1 by A1, Th102;
then A2: the_Vertices_of G1 = the_Vertices_of the spanning acyclic plain Subgraph of G2 by GLIB_000:def 33
.= the_Vertices_of G2 by GLIB_000:def 33 ;

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 = the plain addVertices of createGraph e, the_Vertices_of G2;
not e in G9 .loops() ;
then the plain addVertices of createGraph e, the_Vertices_of G2 in G2 .allSpanningForests() by Th107;
then the plain addVertices of createGraph e, the_Vertices_of G2 is Subgraph of G1 by A1, Th102;
then the_Edges_of the plain addVertices of createGraph e, the_Vertices_of G2 c= the_Edges_of G1 by GLIB_000:def 32;
then the_Edges_of (createGraph e) c= the_Edges_of G1 by GLIB_006:def 10;
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 = the plain addVertices of createGraph e, the_Vertices_of G2;
not e in G9 .loops() ;
then the plain addVertices of createGraph e, the_Vertices_of G2 in G2 .allSpanningForests() by Th107;
then A6: ( the plain addVertices of createGraph e, the_Vertices_of G2 is Subgraph of G1 & the plain addVertices of createGraph e, the_Vertices_of G2 is Subgraph of G2 ) by A1, Th102;
the_Edges_of the plain addVertices of createGraph e, the_Vertices_of G2 = the_Edges_of (createGraph e) by GLIB_006:def 10
.= {e} by Th13 ;
then A7: x in the_Edges_of the plain addVertices of createGraph e, the_Vertices_of G2 by TARSKI:def 1;
thus (the_Source_of G2) . x = (the_Source_of the plain addVertices of createGraph e, the_Vertices_of G2) . x by A6, 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 the plain addVertices of createGraph e, the_Vertices_of G2) . x by A6, A7, GLIB_000:def 32
.= (the_Target_of G1) . x by A6, A7, GLIB_000:def 32 ; :: thesis: verum

end;

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