let G be _Graph; :: thesis: for H being removeLoops of G holds SubtreeRel G = SubtreeRel H
let H be removeLoops of G; :: thesis: SubtreeRel G = SubtreeRel H
thus SubtreeRel G = (SubtreeRel G) |_2 (G .allTrees()) by WELLORD1:21
.= (SubtreeRel G) |_2 (H .allTrees()) by Th146
.= SubtreeRel H by Th162 ; :: thesis: verum