let G be _Graph; :: thesis: field (SubtreeRel G) = G .allTrees()
G .allTrees() c= G .allSG() ;
then G .allTrees() c= field (SubgraphRel G) by Th40;
hence field (SubtreeRel G) = G .allTrees() by ORDERS_1:71; :: thesis: verum