let G1, G2 be _Graph; :: thesis: for G3 being spanning Subgraph of G1 st G2 == G3 holds
G2 is spanning Subgraph of G1
let G3 be spanning Subgraph of G1; :: thesis: ( G2 == G3 implies G2 is spanning Subgraph of G1 )
assume A1: G2 == G3 ; :: thesis: G2 is spanning Subgraph of G1
then the_Vertices_of G2 = the_Vertices_of G1 by Def33;
hence G2 is spanning Subgraph of G1 by A1, Th92, Def33; :: thesis: verum