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 G3 by GLIB_000:def 34
.= the_Vertices_of G1 by GLIB_000:def 33 ;
hence G2 is spanning Subgraph of G1 by A1, GLIB_000:92, GLIB_000:def 33; :: thesis: verum