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