let G1 be _Graph; :: thesis: for G2 being loopless connected _Graph st G2 .allSpanningTrees() c= G1 .allSpanningTrees() holds
G2 is spanning Subgraph of G1
let G2 be loopless connected _Graph; :: thesis: ( G2 .allSpanningTrees() c= G1 .allSpanningTrees() implies G2 is spanning Subgraph of G1 )
assume A1: G2 .allSpanningTrees() c= G1 .allSpanningTrees() ; :: thesis: G2 is spanning Subgraph of G1
set H0 = the spanning Tree-like plain Subgraph of G2;
the spanning Tree-like plain Subgraph of G2 in G2 .allSpanningTrees() by Th168;
then the spanning Tree-like plain Subgraph of G2 is spanning Subgraph of G1 by A1, Th168;
then A2: the_Vertices_of G1 = the_Vertices_of the spanning Tree-like 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
x in (the_Edges_of G2) \ (G2 .loops()) by A3;
then consider T being spanning Tree-like plain Subgraph of G2 such that
A4: x in the_Edges_of T by Th167;
T in G2 .allSpanningTrees() by Th168;
then T is Subgraph of G1 by A1, Th168;
then the_Edges_of T c= the_Edges_of G1 by GLIB_000:def 32;
hence x in the_Edges_of G1 by A4; :: thesis: verum

end;

then A5: 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 A6: 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 )
x in (the_Edges_of G2) \ (G2 .loops()) by A6;
then consider T being spanning Tree-like plain Subgraph of G2 such that
A7: x in the_Edges_of T by Th167;
T in G2 .allSpanningTrees() by Th168;
then A8: T is Subgraph of G1 by A1, Th168;
thus (the_Source_of G2) . x = (the_Source_of T) . x by A7, GLIB_000:def 32
.= (the_Source_of G1) . x by A7, A8, GLIB_000:def 32 ; :: thesis: (the_Target_of G2) . x = (the_Target_of G1) . x
thus (the_Target_of G2) . x = (the_Target_of T) . x by A7, GLIB_000:def 32
.= (the_Target_of G1) . x by A7, A8, GLIB_000:def 32 ; :: thesis: verum

end;

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