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