for G1 being _finite Tree-like _Graph
for G2 being spanning Tree-like Subgraph of G1 holds G1 == G2