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