let G3 be _Graph; :: thesis: for V1, V2 being set
for G2 being addVertices of G3,V2
for G1 being addVertices of G2,V1 holds G1 is addVertices of G3,V1 \/ V2
let V1, V2 be set ; :: thesis: for G2 being addVertices of G3,V2
for G1 being addVertices of G2,V1 holds G1 is addVertices of G3,V1 \/ V2
let G2 be addVertices of G3,V2; :: thesis: for G1 being addVertices of G2,V1 holds G1 is addVertices of G3,V1 \/ V2
let G1 be addVertices of G2,V1; :: thesis: G1 is addVertices of G3,V1 \/ V2
A1: ( the_Vertices_of G1 = (the_Vertices_of G2) \/ V1 & 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;
( the_Vertices_of G2 = (the_Vertices_of G3) \/ V2 & the_Edges_of G2 = the_Edges_of G3 & the_Source_of G2 = the_Source_of G3 & the_Target_of G2 = the_Target_of G3 ) by Def10;
then A3: the_Vertices_of G1 = (the_Vertices_of G3) \/ (V1 \/ V2) by A1, XBOOLE_1:4;
A4: the_Edges_of G1 = the_Edges_of G3 by A1, Def10;
A5: the_Source_of G1 = the_Source_of G3 by A1, Def10;
A6: the_Target_of G1 = the_Target_of G3 by A1, Def10;
G1 is Supergraph of G3 by Th66;
hence G1 is addVertices of G3,V1 \/ V2 by A3, A4, A5, A6, Def10; :: thesis: verum