let G1 be edgeless _Graph; :: thesis: for G2 being Subgraph of G1 holds G1 is addVertices of G2,(the_Vertices_of G1) \ (the_Vertices_of G2)
let G2 be Subgraph of G1; :: thesis: G1 is addVertices of G2,(the_Vertices_of G1) \ (the_Vertices_of G2)
A1: the_Edges_of G1 = the_Edges_of G2 ;
G1 is Supergraph of G2 by GLIB_006:57;
hence G1 is addVertices of G2,(the_Vertices_of G1) \ (the_Vertices_of G2) by A1, Th33; :: thesis: verum