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

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

let x be object ; :: thesis: ( x in H .allSpanningForests() implies x in G .allSpanningForests() )
assume x in H .allSpanningForests() ; :: thesis: x in G .allSpanningForests()
then reconsider H9 = x as spanning acyclic plain Subgraph of H by Th102;
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 .allSpanningForests() by Th102; :: thesis: verum

end;

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