for G1, G2 being _Graph
for G3 being Component of G1 st G2 == G3 holds
G2 is Component of G1