let G3 be _Graph; :: thesis: for V1, V2 being set
for G1 being addVertices of G3,V1 \/ V2 ex G2 being addVertices of G3,V2 st G1 is addVertices of G2,V1
let V1, V2 be set ; :: thesis: for G1 being addVertices of G3,V1 \/ V2 ex G2 being addVertices of G3,V2 st G1 is addVertices of G2,V1
let G1 be addVertices of G3,V1 \/ V2; :: thesis: ex G2 being addVertices of G3,V2 st G1 is addVertices of G2,V1
set G2 = the addVertices of G3,V2;
take the addVertices of G3,V2 ; :: thesis: G1 is addVertices of the addVertices of G3,V2,V1
A1: ( the_Vertices_of the addVertices of G3,V2 = (the_Vertices_of G3) \/ V2 & the_Edges_of the addVertices of G3,V2 = the_Edges_of G3 & the_Source_of the addVertices of G3,V2 = the_Source_of G3 & the_Target_of the addVertices of G3,V2 = the_Target_of G3 ) by Def10;
A2: ( the_Vertices_of G1 = (the_Vertices_of G3) \/ (V1 \/ V2) & the_Edges_of G1 = the_Edges_of G3 & the_Source_of G1 = the_Source_of G3 & the_Target_of G1 = the_Target_of G3 ) by Def10;
(the_Vertices_of G3) \/ V2 c= (the_Vertices_of G3) \/ (V1 \/ V2) by XBOOLE_1:7, XBOOLE_1:9;
then A4: the_Vertices_of the addVertices of G3,V2 c= the_Vertices_of G1 by A1, Def10;
for e being set st e in the_Edges_of the addVertices of G3,V2 holds
( (the_Source_of the addVertices of G3,V2) . e = (the_Source_of G1) . e & (the_Target_of the addVertices of G3,V2) . e = (the_Target_of G1) . e ) by A1, A2;
then A5: G1 is Supergraph of the addVertices of G3,V2 by A1, A2, A4, Def9;
the_Vertices_of G1 = ((the_Vertices_of G3) \/ V2) \/ V1 by A2, XBOOLE_1:4
.= (the_Vertices_of the addVertices of G3,V2) \/ V1 by Def10 ;
hence G1 is addVertices of the addVertices of G3,V2,V1 by A1, A2, A5, Def10; :: thesis: verum