for G1 being _Graph
for G2 being spanning Subgraph of G1
for G3 being spanning Subgraph of G2 holds G3 is spanning Subgraph of G1