for G1, G2 being _Graph
for x being set st G1 == G2 & G1 is_DTree_rooted_at x holds
G2 is_DTree_rooted_at x