let G be connected _Graph; :: thesis: for H being spanning connected Subgraph of G holds H .allSpanningTrees() c= G .allSpanningTrees()
let H be spanning connected Subgraph of G; :: thesis: H .allSpanningTrees() c= G .allSpanningTrees()

now :: thesis: for x being object st x in H .allSpanningTrees() holds
x in G .allSpanningTrees()

let x be object ; :: thesis: ( x in H .allSpanningTrees() implies x in G .allSpanningTrees() )
assume A1: x in H .allSpanningTrees() ; :: thesis: x in G .allSpanningTrees()
then reconsider H9 = x as spanning acyclic plain Subgraph of H by Th168;
the_Vertices_of H9 = the_Vertices_of H by GLIB_000:def 33
.= the_Vertices_of G by GLIB_000:def 33 ;
then H9 is spanning acyclic plain Subgraph of G by GLIB_000:43, GLIB_000:def 33;
hence x in G .allSpanningTrees() by A1, Th168; :: thesis: verum

end;

hence H .allSpanningTrees() c= G .allSpanningTrees() by TARSKI:def 3; :: thesis: verum