let G2 be _Graph; :: thesis: for V being set
for G1 being addVertices of G2,V holds
( G1 == G2 iff V c= the_Vertices_of G2 )
let V be set ; :: thesis: for G1 being addVertices of G2,V holds
( G1 == G2 iff V c= the_Vertices_of G2 )
let G1 be addVertices of G2,V; :: thesis: ( G1 == G2 iff V c= the_Vertices_of G2 )

hereby :: thesis: ( V c= the_Vertices_of G2 implies G1 == G2 )

assume G1 == G2 ; :: thesis: V c= the_Vertices_of G2
then the_Vertices_of G2 = the_Vertices_of G1 by GLIB_000:def 34
.= (the_Vertices_of G2) \/ V by Def10 ;
hence V c= the_Vertices_of G2 by XBOOLE_1:11; :: thesis: verum

end;

assume V c= the_Vertices_of G2 ; :: thesis: G1 == G2
then A1: V \/ (the_Vertices_of G2) c= (the_Vertices_of G2) \/ (the_Vertices_of G2) by XBOOLE_1:9;
the_Vertices_of G2 c= V \/ (the_Vertices_of G2) by XBOOLE_1:7;
then A2: the_Vertices_of G2 = V \/ (the_Vertices_of G2) by A1, XBOOLE_0:def 10
.= the_Vertices_of G1 by Def10 ;
( the_Edges_of G1 = the_Edges_of G2 & the_Source_of G1 = the_Source_of G2 & the_Target_of G1 = the_Target_of G2 ) by Def10;
hence G1 == G2 by A2, GLIB_000:def 34; :: thesis: verum