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