for G1 being connected _Graph
for G2 being Component of G1 holds G1 == G2