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

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

let x be object ; :: thesis: ( x in H .allTrees() implies x in G .allTrees() )
assume x in H .allTrees() ; :: thesis: x in G .allTrees()
then reconsider H9 = x as Tree-like plain Subgraph of H by Th138;
H9 is Subgraph of G by GLIB_000:43;
hence x in G .allTrees() by Th138; :: thesis: verum

end;

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