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

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

let x be object ; :: thesis: ( x in H .allForests() implies x in G .allForests() )
assume x in H .allForests() ; :: thesis: x in G .allForests()
then reconsider H9 = x as acyclic plain Subgraph of H by Th78;
H9 is Subgraph of G by GLIB_000:43;
hence x in G .allForests() by Th78; :: thesis: verum

end;

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