let G be _Graph; :: thesis: for H being Subgraph of G holds SubtreeRel H = (SubtreeRel G) |_2 (H .allTrees())
let H be Subgraph of G; :: thesis: SubtreeRel H = (SubtreeRel G) |_2 (H .allTrees())
thus SubtreeRel H = ((SubgraphRel G) |_2 (H .allSG())) |_2 (H .allTrees()) by Th43
.= (SubgraphRel G) |_2 ((H .allSG()) /\ (H .allTrees())) by WELLORD1:19
.= (SubgraphRel G) |_2 (H .allTrees()) by XBOOLE_1:28
.= (SubgraphRel G) |_2 ((G .allTrees()) /\ (H .allTrees())) by Th144, XBOOLE_1:28
.= (SubtreeRel G) |_2 (H .allTrees()) by WELLORD1:19 ; :: thesis: verum