let G be _Graph; :: thesis: for H1, H2 being Tree-like plain Subgraph of G holds
( [H1,H2] in SubtreeRel G iff H1 is Subgraph of H2 )
let H1, H2 be Tree-like plain Subgraph of G; :: thesis: ( [H1,H2] in SubtreeRel G iff H1 is Subgraph of H2 )
A1: ( H1 in G .allSG() & H2 in G .allSG() ) by Th1;

hereby :: thesis: ( H1 is Subgraph of H2 implies [H1,H2] in SubtreeRel G )

assume [H1,H2] in SubtreeRel G ; :: thesis: H1 is Subgraph of H2
then [H1,H2] in SubgraphRel G by MMLQUER2:4;
hence H1 is Subgraph of H2 by A1, Def6; :: thesis: verum

end;

A2: ( H1 in G .allTrees() & H2 in G .allTrees() ) by Th138;
assume H1 is Subgraph of H2 ; :: thesis: [H1,H2] in SubtreeRel G
then [H1,H2] in SubgraphRel G by A1, Def6;
hence [H1,H2] in SubtreeRel G by A2, MMLQUER2:4; :: thesis: verum