let G2 be _Graph; :: thesis: for G1 being Supergraph of G2 st the_Edges_of G1 = the_Edges_of G2 holds
G1 is addVertices of G2,(the_Vertices_of G1) \ (the_Vertices_of G2)
let G1 be Supergraph of G2; :: thesis: ( the_Edges_of G1 = the_Edges_of G2 implies G1 is addVertices of G2,(the_Vertices_of G1) \ (the_Vertices_of G2) )
assume A1: the_Edges_of G1 = the_Edges_of G2 ; :: thesis: G1 is addVertices of G2,(the_Vertices_of G1) \ (the_Vertices_of G2)
the_Vertices_of G2 c= the_Vertices_of G1 by GLIB_006:def 9;
then A2: the_Vertices_of G1 = (the_Vertices_of G2) \/ ((the_Vertices_of G1) \ (the_Vertices_of G2)) by XBOOLE_1:45;
A3: the_Source_of G2 = (the_Source_of G1) | (the_Edges_of G2) by GLIB_006:69
.= the_Source_of G1 by A1 ;
the_Target_of G2 = (the_Target_of G1) | (the_Edges_of G2) by GLIB_006:69
.= the_Target_of G1 by A1 ;
hence G1 is addVertices of G2,(the_Vertices_of G1) \ (the_Vertices_of G2) by A1, A2, A3, GLIB_006:def 10; :: thesis: verum